package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Hook : sig ... end
module CInfo : sig ... end
module Info : sig ... end
val declare_definition : info:Info.t -> cinfo:EConstr.t option CInfo.t -> opaque:bool -> body:EConstr.t -> Evd.evar_map -> Names.GlobRef.t
val declare_assumption : name:Names.Id.t -> scope:Locality.locality -> hook:Hook.t option -> impargs:Impargs.manual_implicits -> uctx:UState.t -> Entries.parameter_entry -> Names.GlobRef.t
type lemma_possible_guards = int list list
val declare_mutually_recursive : info:Info.t -> cinfo:Constr.t CInfo.t list -> opaque:bool -> ntns:Vernacexpr.decl_notation list -> uctx:UState.t -> rec_declaration:Constr.rec_declaration -> possible_indexes:lemma_possible_guards option -> Names.GlobRef.t list
module OblState : sig ... end
module Proof : sig ... end
type 'a proof_entry
val definition_entry : ?opaque:bool -> ?using:Names.Id.Set.t -> ?inline:bool -> ?types:Constr.types -> ?univs:Entries.universes_entry -> Constr.constr -> Evd.side_effects proof_entry
val declare_entry : name:Names.Id.t -> scope:Locality.locality -> kind:Decls.logical_kind -> ?hook:Hook.t -> impargs:Impargs.manual_implicits -> uctx:UState.t -> Evd.side_effects proof_entry -> Names.GlobRef.t
val declare_variable : name:Names.variable -> kind:Decls.logical_kind -> typ:Constr.types -> impl:Glob_term.binding_kind -> unit
type !'a constant_entry =
  1. | DefinitionEntry of 'a proof_entry
  2. | ParameterEntry of Entries.parameter_entry
  3. | PrimitiveEntry of Entries.primitive_entry
val prepare_parameter : poly:bool -> udecl:UState.universe_decl -> types:EConstr.types -> Evd.evar_map -> Evd.evar_map * Entries.parameter_entry
val definition_message : Names.Id.t -> unit
val assumption_message : Names.Id.t -> unit
val fixpoint_message : int array option -> Names.Id.t list -> unit
val check_exists : Names.Id.t -> unit
val build_by_tactic : ?side_eff:bool -> Environ.env -> uctx:UState.t -> poly:bool -> typ:EConstr.types -> unit Proofview.tactic -> Constr.constr * Constr.types option * Entries.universes_entry * bool * UState.t
module Obls : sig ... end
module Internal : sig ... end