diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-07 00:48:14 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-07 00:53:19 +0100 |
commit | 9402b6efad32757f44d72d83f6aabdca8829e3ed (patch) | |
tree | 0ab9fc18568664e4b7bd0a63f9b52c6303e73a61 /proofs | |
parent | 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff) |
[api] Remove 8.7 ML-deprecated functions.
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/pfedit.ml | 28 | ||||
-rw-r--r-- | proofs/pfedit.mli | 82 |
2 files changed, 0 insertions, 110 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 469e1a011..2d4aba17c 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -230,31 +230,3 @@ let apply_implicit_tactic tac = (); fun env sigma evk -> let solve_by_implicit_tactic () = match !implicit_tactic with | None -> None | Some tac -> Some (apply_implicit_tactic tac) - -(** Deprecated functions *) -let refining = Proof_global.there_are_pending_proofs -let check_no_pending_proofs = Proof_global.check_no_pending_proof - -let get_current_proof_name = Proof_global.get_current_proof_name -let get_all_proof_names = Proof_global.get_all_proof_names - -type lemma_possible_guards = Proof_global.lemma_possible_guards - -let delete_proof = Proof_global.discard -let delete_current_proof = Proof_global.discard_current -let delete_all_proofs = Proof_global.discard_all - -let get_pftreestate () = - Proof_global.give_me_the_proof () - -let set_end_tac tac = - Proof_global.set_endline_tactic tac - -let set_used_variables l = - Proof_global.set_used_variables l - -let get_used_variables () = - Proof_global.get_used_variables () - -let get_universe_decl () = - Proof_global.get_universe_decl () diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 6e4ecd13b..adfe33786 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -8,7 +8,6 @@ (** Global proof state. A quite redundant wrapper on {!Proof_global}. *) -open Loc open Names open Term open Environ @@ -122,84 +121,3 @@ 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_decl : unit -> Univdecls.universe_decl -[@@ocaml.deprecated "use Proof_global.get_universe_decl"] - -(** {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"] |