diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof.ml | 5 | ||||
| -rw-r--r-- | proofs/proof.mli | 4 | ||||
| -rw-r--r-- | proofs/proof_bullet.ml | 3 | ||||
| -rw-r--r-- | proofs/proof_bullet.mli | 6 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 2 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 5 | ||||
| -rw-r--r-- | proofs/refiner.mli | 8 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 9 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 11 |
10 files changed, 3 insertions, 51 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 8bbd82bb0a..70a08e4966 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -122,8 +122,6 @@ type t = { initial_euctx : UState.t } -type proof = t - (*** General proof functions ***) let proof p = @@ -435,9 +433,6 @@ let pr_proof p = (*** Compatibility layer with <=v8.2 ***) module V82 = struct - let subgoals p = - let it, sigma = Proofview.proofview p.proofview in - Evd.{ it; sigma } let background_subgoals p = let it, sigma = Proofview.proofview (unroll_focus p.proofview p.focus_stack) in diff --git a/proofs/proof.mli b/proofs/proof.mli index 511dcc2e00..8cf543557b 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -33,8 +33,6 @@ (* Type of a proof. *) type t -type proof = t -[@@ocaml.deprecated "please use [Proof.t]"] (* Returns a stylised view of a proof for use by, for instance, ide-s. *) @@ -192,8 +190,6 @@ val pr_proof : t -> Pp.t (*** Compatibility layer with <=v8.2 ***) module V82 : sig - val subgoals : t -> Goal.goal list Evd.sigma - [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"] (* All the subgoals of the proof, including those which are not focused. *) val background_subgoals : t -> Goal.goal list Evd.sigma diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index cc3e79f858..ed8df29d7b 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -197,6 +197,3 @@ let put p b = let suggest p = (!current_behavior).suggest p - -let pr_goal_selector = Goal_select.pr_goal_selector -let get_default_goal_selector = Goal_select.get_default_goal_selector diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli index a09a7ec1d2..0fcc647a6f 100644 --- a/proofs/proof_bullet.mli +++ b/proofs/proof_bullet.mli @@ -44,9 +44,3 @@ val register_behavior : behavior -> unit *) val put : Proof.t -> t -> Proof.t val suggest : Proof.t -> Pp.t - -(** Deprecated *) -val pr_goal_selector : Goal_select.t -> Pp.t -[@@ocaml.deprecated "Please use [Goal_select.pr_goal_selector]"] -val get_default_goal_selector : unit -> Goal_select.t -[@@ocaml.deprecated "Please use [Goal_select.get_default_goal_selector]"] diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 7e250faa86..de151fb6e5 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -101,7 +101,6 @@ type pstate = { } type t = pstate list -type state = t let make_terminator f = f let apply_terminator f = f diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 854ceaa41a..2b04bfab57 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -13,8 +13,6 @@ environment. *) type t -type state = t -[@@ocaml.deprecated "please use [Proof_global.t]"] val there_are_pending_proofs : unit -> bool val check_no_pending_proof : unit -> unit diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 1350da65dc..56ce744bc1 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -15,7 +15,6 @@ open Names open Constr open EConstr open Declarations -open Globnames open Genredexpr open Pattern open Reductionops @@ -79,7 +78,7 @@ let set_strategy_one ref l = | OpaqueDef _ -> user_err ~hdr:"set_transparent_const" (str "Cannot make" ++ spc () ++ - Nametab.pr_global_env Id.Set.empty (ConstRef sp) ++ + Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef sp) ++ spc () ++ str "transparent because it was declared opaque."); | _ -> Csymtable.set_transparent_const sp) | _ -> () @@ -115,7 +114,7 @@ let classify_strategy (local,_ as obj) = let disch_ref ref = match ref with EvalConstRef c -> Some ref - | EvalVarRef id -> if Lib.is_in_section (VarRef id) then None else Some ref + | EvalVarRef id -> if Lib.is_in_section (GlobRef.VarRef id) then None else Some ref let discharge_strategy (_,(local,obj)) = if local then None else diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 0f83e16ec8..30af6d8e1a 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -22,14 +22,6 @@ val project : 'a sigma -> evar_map val pf_env : goal sigma -> Environ.env val pf_hyps : goal sigma -> named_context -val unpackage : 'a sigma -> evar_map ref * 'a -[@@ocaml.deprecated "Do not use [evar_map ref]"] -val repackage : evar_map ref -> 'a -> 'a sigma -[@@ocaml.deprecated "Do not use [evar_map ref]"] -val apply_sig_tac : - evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list -[@@ocaml.deprecated "Do not use [evar_map ref]"] - val refiner : rule -> tactic (** {6 Tacticals. } *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 9e42a71ea8..5d1faf1465 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -30,14 +30,7 @@ let re_sig it gc = { it = it; sigma = gc; } (* Operations for handling terms under a local typing context *) (**************************************************************) -type 'a sigma = 'a Evd.sigma;; -type tactic = Proof_type.tactic;; - -[@@@ocaml.warning "-3"] -let unpackage = Refiner.unpackage -let repackage = Refiner.repackage -let apply_sig_tac = Refiner.apply_sig_tac -[@@@ocaml.warning "+3"] +type tactic = Proof_type.tactic let sig_it = Refiner.sig_it let project = Refiner.project diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index b4cb2be2b8..3432ad4afa 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -18,9 +18,6 @@ open Locus (** Operations for handling terms under a local typing context. *) -type 'a sigma = 'a Evd.sigma -[@@ocaml.deprecated "alias of Evd.sigma"] - open Evd type tactic = Proof_type.tactic;; @@ -29,14 +26,6 @@ val project : goal sigma -> evar_map val re_sig : 'a -> evar_map -> 'a sigma -val unpackage : 'a sigma -> evar_map ref * 'a -[@@ocaml.deprecated "Do not use [evar_map ref]"] -val repackage : evar_map ref -> 'a -> 'a sigma -[@@ocaml.deprecated "Do not use [evar_map ref]"] -val apply_sig_tac : - evar_map ref -> (goal sigma -> (goal list) sigma) -> goal -> (goal list) -[@@ocaml.deprecated "Do not use [evar_map ref]"] - val pf_concl : goal sigma -> types val pf_env : goal sigma -> env val pf_hyps : goal sigma -> named_context |