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 /proofs/pfedit.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 'proofs/pfedit.mli')
-rw-r--r-- | proofs/pfedit.mli | 157 |
1 files changed, 86 insertions, 71 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 1bf65b8ae..f009593e9 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -14,39 +14,6 @@ open Term open Environ open Decl_kinds -(** Several proofs can be opened simultaneously but at most one is - focused at some time. The following functions work by side-effect - on current set of open proofs. In this module, ``proofs'' means an - open proof (something started by vernacular command [Goal], [Lemma] - or [Theorem]), and ``goal'' means a subgoal of the current focused - proof *) - -(** {6 ... } *) -(** [refining ()] tells if there is some proof in progress, even if a not - focused one *) - -val refining : unit -> bool - -(** [check_no_pending_proofs ()] fails if there is still some proof in - progress *) - -val check_no_pending_proofs : unit -> unit - -(** {6 ... } *) -(** [delete_proof name] deletes proof of name [name] or fails if no proof - has this name *) - -val delete_proof : Id.t located -> unit - -(** [delete_current_proof ()] deletes current focused proof or fails if - no proof is focused *) - -val delete_current_proof : unit -> unit - -(** [delete_all_proofs ()] deletes all open proofs if any *) - -val delete_all_proofs : unit -> unit - (** {6 ... } *) (** [start_proof s str env t hook tac] starts a proof of name [s] and conclusion [t]; [hook] is optionally a function to be applied at @@ -55,12 +22,8 @@ val delete_all_proofs : unit -> unit systematically apply at initialization time (e.g. to start the proof of mutually dependent theorems) *) -type lemma_possible_guards = Proof_global.lemma_possible_guards - -type universe_binders = Id.t Loc.located list - val start_proof : - Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr -> + Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr -> ?init_tac:unit Proofview.tactic -> Proof_global.proof_terminator -> unit @@ -80,11 +43,6 @@ val cook_proof : unit -> (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) (** {6 ... } *) -(** [get_pftreestate ()] returns the current focused pending proof. - @raise NoCurrentProof if there is no pending proof. *) - -val get_pftreestate : unit -> Proof.proof - (** [get_goal_context n] returns the context of the [n]th subgoal of the current focused proof or raises a [UserError] if there is no focused proof or if there is no more subgoals *) @@ -109,34 +67,6 @@ val current_proof_statement : unit -> Id.t * goal_kind * EConstr.types (** {6 ... } *) -(** [get_current_proof_name ()] return the name of the current focused - proof or failed if no proof is focused *) - -val get_current_proof_name : unit -> Id.t - -(** [get_all_proof_names ()] returns the list of all pending proof names. - The first name is the current proof, the other names may come in - any order. *) - -val get_all_proof_names : unit -> Id.t list - -(** {6 ... } *) -(** [set_end_tac tac] applies tactic [tac] to all subgoal generate - by [solve] *) - -val set_end_tac : Genarg.glob_generic_argument -> unit - -(** {6 ... } *) -(** [set_used_variables l] declares that section variables [l] will be - used in the proof *) -val set_used_variables : - Id.t list -> Context.Named.t * Names.Id.t Loc.located list -val get_used_variables : unit -> Context.Named.t option - -(** {6 Universe binders } *) -val get_universe_binders : unit -> universe_binders option - -(** {6 ... } *) (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th subgoal of the current focused proof or raises a [UserError] if no proof is focused or if there is no [n]th subgoal. [solve SelectAll @@ -191,3 +121,88 @@ val clear_implicit_tactic : unit -> unit (* Raise Exit if cannot solve *) val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option + +(** {5 Deprecated functions in favor of [Proof_global]} *) + +(** {6 ... } *) +(** Several proofs can be opened simultaneously but at most one is + focused at some time. The following functions work by side-effect + on current set of open proofs. In this module, ``proofs'' means an + open proof (something started by vernacular command [Goal], [Lemma] + or [Theorem]), and ``goal'' means a subgoal of the current focused + proof *) + +(** [refining ()] tells if there is some proof in progress, even if a not + focused one *) + +val refining : unit -> bool +[@@ocaml.deprecated "use Proof_global.there_are_pending_proofs"] + +(** [check_no_pending_proofs ()] fails if there is still some proof in + progress *) + +val check_no_pending_proofs : unit -> unit +[@@ocaml.deprecated "use Proof_global.check_no_pending_proofs"] + +(** {6 ... } *) +(** [delete_proof name] deletes proof of name [name] or fails if no proof + has this name *) + +val delete_proof : Id.t located -> unit +[@@ocaml.deprecated "use Proof_global.discard"] + +(** [delete_current_proof ()] deletes current focused proof or fails if + no proof is focused *) + +val delete_current_proof : unit -> unit +[@@ocaml.deprecated "use Proof_global.discard_current"] + +(** [delete_all_proofs ()] deletes all open proofs if any *) +val delete_all_proofs : unit -> unit +[@@ocaml.deprecated "use Proof_global.discard_all"] + +(** [get_pftreestate ()] returns the current focused pending proof. + @raise NoCurrentProof if there is no pending proof. *) + +val get_pftreestate : unit -> Proof.proof +[@@ocaml.deprecated "use Proof_global.give_me_the_proof"] + +(** {6 ... } *) +(** [set_end_tac tac] applies tactic [tac] to all subgoal generate + by [solve] *) + +val set_end_tac : Genarg.glob_generic_argument -> unit +[@@ocaml.deprecated "use Proof_global.set_endline_tactic"] + +(** {6 ... } *) +(** [set_used_variables l] declares that section variables [l] will be + used in the proof *) +val set_used_variables : + Id.t list -> Context.Named.t * Names.Id.t Loc.located list +[@@ocaml.deprecated "use Proof_global.set_used_variables"] + +val get_used_variables : unit -> Context.Named.t option +[@@ocaml.deprecated "use Proof_global.get_used_variables"] + +(** {6 Universe binders } *) +val get_universe_binders : unit -> Proof_global.universe_binders option +[@@ocaml.deprecated "use Proof_global.get_universe_binders"] + +(** {6 ... } *) +(** [get_current_proof_name ()] return the name of the current focused + proof or failed if no proof is focused *) +val get_current_proof_name : unit -> Id.t +[@@ocaml.deprecated "use Proof_global.get_current_proof_name"] + +(** [get_all_proof_names ()] returns the list of all pending proof names. + The first name is the current proof, the other names may come in + any order. *) +val get_all_proof_names : unit -> Id.t list +[@@ocaml.deprecated "use Proof_global.get_all_proof_names"] + +type lemma_possible_guards = Proof_global.lemma_possible_guards +[@@ocaml.deprecated "use Proof_global.lemma_possible_guards"] + +type universe_binders = Proof_global.universe_binders +[@@ocaml.deprecated "use Proof_global.universe_binders"] + |