diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-13 19:03:03 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-13 19:03:03 +0100 |
| commit | ed0c434a05a929a659e43aed80ab7c8179a7daa3 (patch) | |
| tree | d486bf54f6bbfd6ace8dc9cea52b959699f88ebe /vernac/lemmas.mli | |
| parent | c571cdbbcac5cb4b4a5a19ab2f7ac51222316292 (diff) | |
[api] Insert miscellaneous API deprecation back to core.
Diffstat (limited to 'vernac/lemmas.mli')
| -rw-r--r-- | vernac/lemmas.mli | 6 |
1 files changed, 3 insertions, 3 deletions
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 : |