coq 8.12.2 · OCaml Package

module Proof : sig ... end

type opacity_flag = Vernacexpr.opacity_flag =

| Opaque
| Transparent

val start_proof : 
  name:Names.Id.t ->
  udecl:UState.universe_decl ->
  poly:bool ->
  Evd.evar_map ->
  (Environ.env * EConstr.types) list ->
  Proof.t

val start_dependent_proof : 
  name:Names.Id.t ->
  udecl:UState.universe_decl ->
  poly:bool ->
  Proofview.telescope ->
  Proof.t

type !'a proof_entry = private {

proof_entry_body : 'a Entries.const_entry_body;
proof_entry_secctx : Names.Id.Set.t option;
proof_entry_feedback : Stateid.t option;
proof_entry_type : Constr.types option;
proof_entry_universes : Entries.universes_entry;
proof_entry_opaque : bool;
proof_entry_inline_code : bool;

}

type proof_object = private {

name : Names.Id.t;
entries : Evd.side_effects proof_entry list;
uctx : UState.t;

}

val close_proof : 
  opaque:opacity_flag ->
  keep_body_ucst_separate:bool ->
  Proof.t ->
  proof_object

type variable_declaration =

| SectionLocalDef of Evd.side_effects proof_entry
| SectionLocalAssum of {
1. typ : Constr.types;
2. impl : Glob_term.binding_kind;
}

type !'a constant_entry =

| DefinitionEntry of 'a proof_entry
| ParameterEntry of Entries.parameter_entry
| PrimitiveEntry of Entries.primitive_entry

val declare_variable : 
  name:Names.variable ->
  kind:Decls.logical_kind ->
  variable_declaration ->
  unit

val definition_entry : 
  ?fix_exn:Future.fix_exn ->
  ?opaque:bool ->
  ?inline:bool ->
  ?feedback_id:Stateid.t ->
  ?section_vars:Names.Id.Set.t ->
  ?types:Constr.types ->
  ?univs:Entries.universes_entry ->
  ?eff:Evd.side_effects ->
  ?univsbody:Univ.ContextSet.t ->
  Constr.constr ->
  Evd.side_effects proof_entry

type import_status =

| ImportDefaultBehavior
| ImportNeedQualified

val declare_constant : 
  ?local:import_status ->
  name:Names.Id.t ->
  kind:Decls.logical_kind ->
  Evd.side_effects constant_entry ->
  Names.Constant.t

val inline_private_constants : 
  uctx:UState.t ->
  Environ.env ->
  Evd.side_effects proof_entry ->
  Constr.t * UState.t

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

module Internal : sig ... end

type closed_proof_output

val return_proof : Proof.t -> closed_proof_output

val return_partial_proof : Proof.t -> closed_proof_output

val close_future_proof : 
  feedback_id:Stateid.t ->
  Proof.t ->
  closed_proof_output Future.computation ->
  proof_object

val by : unit Proofview.tactic -> Proof.t -> Proof.t * bool

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

val get_goal_context : Proof.t -> int -> Evd.evar_map * Environ.env

val get_current_goal_context : Proof.t -> Evd.evar_map * Environ.env

val get_current_context : Proof.t -> Evd.evar_map * Environ.env

val build_constant_by_tactic : 
  name:Names.Id.t ->
  ?opaque:opacity_flag ->
  uctx:UState.t ->
  sign:Environ.named_context_val ->
  poly:bool ->
  EConstr.types ->
  unit Proofview.tactic ->
  Evd.side_effects proof_entry * bool * UState.t

val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit

deprecated Use DeclareUctx.declare_universe_context

type locality =

| Discharge
| Global of import_status

module Hook : sig ... end

val declare_entry : 
  name:Names.Id.t ->
  scope:locality ->
  kind:Decls.logical_kind ->
  ?hook:Hook.t ->
  ?obls:(Names.Id.t * Constr.t) list ->
  impargs:Impargs.manual_implicits ->
  uctx:UState.t ->
  Evd.side_effects proof_entry ->
  Names.GlobRef.t

val declare_definition : 
  name:Names.Id.t ->
  scope:locality ->
  kind:Decls.logical_kind ->
  opaque:bool ->
  impargs:Impargs.manual_implicits ->
  udecl:UState.universe_decl ->
  ?hook:Hook.t ->
  ?obls:(Names.Id.t * Constr.t) list ->
  poly:bool ->
  ?inline:bool ->
  types:EConstr.t option ->
  body:EConstr.t ->
  ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) ->
  Evd.evar_map ->
  Names.GlobRef.t

val declare_assumption : 
  ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) ->
  name:Names.Id.t ->
  scope:locality ->
  hook:Hook.t option ->
  impargs:Impargs.manual_implicits ->
  uctx:UState.t ->
  Entries.parameter_entry ->
  Names.GlobRef.t

module Recthm : sig ... end

val declare_mutually_recursive : 
  opaque:bool ->
  scope:locality ->
  kind:Decls.logical_kind ->
  poly:bool ->
  uctx:UState.t ->
  udecl:UState.universe_decl ->
  ntns:Vernacexpr.decl_notation list ->
  rec_declaration:Constr.rec_declaration ->
  possible_indexes:int list list option ->
  ?restrict_ucontext:bool ->
  Recthm.t list ->
  Names.GlobRef.t list

val prepare_obligation : 
  ?opaque:bool ->
  ?inline:bool ->
  name:Names.Id.t ->
  poly:bool ->
  udecl:UState.universe_decl ->
  types:EConstr.t option ->
  body:EConstr.t ->
  Evd.evar_map ->
  Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info

val prepare_parameter : 
  poly:bool ->
  udecl:UState.universe_decl ->
  types:EConstr.types ->
  Evd.evar_map ->
  Evd.evar_map * Entries.parameter_entry

exception AlreadyDeclared of string option * Names.Id.t

package coq