diff options
Diffstat (limited to 'stm/lemmas.mli')
| -rw-r--r-- | stm/lemmas.mli | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/stm/lemmas.mli b/stm/lemmas.mli index 6556aa22..16e54e31 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <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 *) @@ -14,7 +14,6 @@ open Vernacexpr open Pfedit type 'a declaration_hook - val mk_hook : (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook @@ -24,20 +23,24 @@ val call_hook : (** 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 -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types -> +val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> + ?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 -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types -> +val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> + ?sign:Environ.named_context_val -> types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> - (Proof_global.proof_universes option -> unit declaration_hook) -> unit + (Evd.evar_universe_context option -> unit declaration_hook) -> unit val start_proof_com : 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 * (types * (Name.t list * Impargs.manual_explicitation list))) list + 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 standard_proof_terminator : |