From ed0c434a05a929a659e43aed80ab7c8179a7daa3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 13 Nov 2017 19:03:03 +0100 Subject: [api] Insert miscellaneous API deprecation back to core. --- vernac/lemmas.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'vernac/lemmas.mli') diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 1f46a385d..6972edd52 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -27,10 +27,10 @@ val start_proof : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_m 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 -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) -> + ?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 -> - (Evd.evar_universe_context option -> unit declaration_hook) -> unit + (UState.t option -> unit declaration_hook) -> unit val start_proof_com : ?inference_hook:Pretyping.inference_hook -> @@ -46,7 +46,7 @@ val start_proof_with_initialization : val universe_proof_terminator : Proof_global.lemma_possible_guards -> - (Evd.evar_universe_context option -> unit declaration_hook) -> + (UState.t option -> unit declaration_hook) -> Proof_global.proof_terminator val standard_proof_terminator : -- cgit v1.2.3