Module Lemmas
type declaration_hook
type hook_type
= UState.t -> (Names.Id.t * Constr.t) list -> Decl_kinds.locality -> Names.GlobRef.t -> unit
hook_type
passes to the client:ustate
: universe constraints obtained when the term was closed(n1,t1),...(nm,tm)
: association list between obligation name and the corresponding defined term (might be a constant, but also an arbitrary term in the Expand case of obligations)locality
: Locality of the original declarationref
: identifier of the origianl declaration
val mk_hook : hook_type -> declaration_hook
val call_hook : ?hook:declaration_hook -> ?fix_exn:Future.fix_exn -> hook_type
val start_proof : ontop:Proof_global.t option -> Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> Evd.evar_map -> ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> ?compute_guard:Proof_global.lemma_possible_guards -> ?hook:declaration_hook -> EConstr.types -> Proof_global.t
val start_proof_com : program_mode:bool -> ontop:Proof_global.t option -> ?inference_hook:Pretyping.inference_hook -> ?hook:declaration_hook -> Decl_kinds.goal_kind -> Vernacexpr.proof_expr list -> Proof_global.t
val start_proof_with_initialization : ontop:Proof_global.t option -> ?hook:declaration_hook -> Decl_kinds.goal_kind -> Evd.evar_map -> UState.universe_decl -> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option -> (Names.Id.t * (EConstr.types * (Names.Name.t list * Impargs.manual_explicitation list))) list -> int list option -> Proof_global.t
val standard_proof_terminator : ?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator
val fresh_name_for_anonymous_theorem : pstate:Proof_global.t option -> Names.Id.t
val initialize_named_context_for_proof : unit -> Environ.named_context_val
...
val save_proof_admitted : ?proof:Proof_global.closed_proof -> pstate:Proof_global.t -> unit
val save_proof_proved : ?proof:Proof_global.closed_proof -> ?pstate:Proof_global.t -> opaque:Proof_global.opacity_flag -> idopt:Names.lident option -> Proof_global.t option