diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-11 06:08:02 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-11 15:54:48 +0200 |
| commit | f610068823b33bdc0af752a646df05b98489d7ce (patch) | |
| tree | 5d664bd1b3efb43536250b30b0dffa724e28dba4 /vernac/lemmas.mli | |
| parent | 79c42e22dd5106dcb85229ceec75331029ab5486 (diff) | |
[proof] Deprecate redundant wrappers.
As we would like to reduce the role of proof_global in future
versions, we start to deprecate old compatibility aliases in `Pfedit`
in favor of the real functions underlying the 8.5 proof engine.
We also deprecate a couple of alias types and explicitly mark the few
remaining uses of `Pfedit`.
Diffstat (limited to 'vernac/lemmas.mli')
| -rw-r--r-- | vernac/lemmas.mli | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index d06b8fd14..a9c0d99f3 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -9,7 +9,6 @@ open Names open Term open Decl_kinds -open Pfedit type 'a declaration_hook val mk_hook : @@ -21,16 +20,16 @@ val call_hook : (** A hook start_proof calls on the type of the definition being started *) val set_start_hook : (EConstr.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) -> +val start_proof : Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map -> + ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> - ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> + ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.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) -> +val start_proof_univs : Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map -> + ?terminator:(Proof_global.lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> - ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> + ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> unit val start_proof_com : @@ -40,8 +39,8 @@ val start_proof_com : val start_proof_with_initialization : goal_kind -> Evd.evar_map -> - (bool * lemma_possible_guards * unit Proofview.tactic list option) option -> - ((Id.t (* name of thm *) * universe_binders option) * + (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option -> + ((Id.t (* name of thm *) * Proof_global.universe_binders option) * (types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit |