diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /stm/lemmas.mli | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'stm/lemmas.mli')
-rw-r--r-- | stm/lemmas.mli | 69 |
1 files changed, 0 insertions, 69 deletions
diff --git a/stm/lemmas.mli b/stm/lemmas.mli deleted file mode 100644 index 39c089be..00000000 --- a/stm/lemmas.mli +++ /dev/null @@ -1,69 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open Term -open Decl_kinds -open Pfedit - -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 : (types -> unit) -> unit - -val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> - ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> - ?sign:Environ.named_context_val -> types -> - ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> - unit declaration_hook -> unit - -val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> - ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) -> - ?sign:Environ.named_context_val -> types -> - ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> - (Evd.evar_universe_context 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 -> - (bool * lemma_possible_guards * unit Proofview.tactic list option) option -> - ((Id.t * universe_binders option) * - (types * (Name.t list * Impargs.manual_explicitation list))) list - -> int list option -> unit declaration_hook -> unit - -val universe_proof_terminator : - Proof_global.lemma_possible_guards -> - (Evd.evar_universe_context option -> unit declaration_hook) -> - Proof_global.proof_terminator - -val standard_proof_terminator : - Proof_global.lemma_possible_guards -> unit declaration_hook -> - Proof_global.proof_terminator - -(** {6 ... } *) - -(** A hook the next three functions pass to cook_proof *) -val set_save_hook : (Proof.proof -> 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 |