diff options
Diffstat (limited to 'vernac/lemmas.mli')
-rw-r--r-- | vernac/lemmas.mli | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli new file mode 100644 index 00000000..ad4c278e --- /dev/null +++ b/vernac/lemmas.mli @@ -0,0 +1,72 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Decl_kinds + +type 'a declaration_hook +val mk_hook : + (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook + +val call_hook : + Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a + +(** A hook start_proof calls on the type of the definition being started *) +val set_start_hook : (EConstr.types -> unit) -> unit + +val start_proof : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> + ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> + ?sign:Environ.named_context_val -> EConstr.types -> + ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> + unit declaration_hook -> unit + +val start_proof_univs : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> + ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> unit declaration_hook) -> Proof_global.proof_terminator) -> + ?sign:Environ.named_context_val -> EConstr.types -> + ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> + (UState.t option -> unit declaration_hook) -> unit + +val start_proof_com : + ?inference_hook:Pretyping.inference_hook -> + goal_kind -> Vernacexpr.proof_expr list -> + unit declaration_hook -> unit + +val start_proof_with_initialization : + goal_kind -> Evd.evar_map -> Univdecls.universe_decl -> + (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option -> + (Id.t (* name of thm *) * + (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list + -> int list option -> unit declaration_hook -> unit + +val universe_proof_terminator : + Proof_global.lemma_possible_guards -> + (UState.t option -> unit declaration_hook) -> + Proof_global.proof_terminator + +val standard_proof_terminator : + Proof_global.lemma_possible_guards -> unit declaration_hook -> + Proof_global.proof_terminator + +val fresh_name_for_anonymous_theorem : unit -> Id.t + +(** {6 ... } *) + +(** A hook the next three functions pass to cook_proof *) +val set_save_hook : (Proof.t -> unit) -> unit + +val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit + + +(** [get_current_context ()] returns the evar context and env of the + current open proof if any, otherwise returns the empty evar context + and the current global env *) + +val get_current_context : unit -> Evd.evar_map * Environ.env +[@@ocaml.deprecated "please use [Pfedit.get_current_context]"] |