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 declaration
  • ref: 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