diff options
Diffstat (limited to 'stm/lemmas.mli')
| -rw-r--r-- | stm/lemmas.mli | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/stm/lemmas.mli b/stm/lemmas.mli index dca6afe19b..e2ddf79df8 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -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,29 +23,31 @@ 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 -> +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 -> goal_kind -> Evd.evar_map -> - ?terminator:(lemma_possible_guards -> (Proof_global.proof_universes option -> unit declaration_hook) -> Proof_global.proof_terminator) -> +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 -> - (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 universe_proof_terminator : Proof_global.lemma_possible_guards -> - (Proof_global.proof_universes option -> unit declaration_hook) -> + (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator val standard_proof_terminator : |