Deprecate Refiner [evar_map ref] exported functions.

Uses internal to Refiner remain.

6 files changed, 14 insertions, 10 deletions

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 6e17e8e15..c6beb08c5 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -184,9 +184,7 @@ let havetac ist
      let gs =
        List.map (fun (_,a) ->
          Ssripats.Internal.pf_find_abstract_proof false gl (EConstr.Unsafe.to_constr a.(1))) skols_args in
-     let tacopen_skols gl =
-        let stuff, g = Refiner.unpackage gl in
-        Refiner.repackage stuff (gs @ [g]) in
+     let tacopen_skols gl = re_sig (gs @ [gl.Evd.it]) gl.Evd.sigma in
      let gl, ty = pf_e_type_of gl t in
      gl, ty, Proofview.V82.of_tactic (Tactics.apply t), id,
        Tacticals.tclTHEN (Tacticals.tclTHEN itac_c simpltac)
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 9cc4f5cec..937e68b06 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -32,9 +32,8 @@ let get_index = function ArgArg i -> i | _ ->
 
 let tclPERM perm tac gls =
   let subgls = tac gls in
-  let sigma, subgll = Refiner.unpackage subgls in
-  let subgll' = perm subgll in
-  Refiner.repackage sigma subgll'
+  let subgll' = perm subgls.Evd.it in
+  re_sig subgll' subgls.Evd.sigma
 
 let rot_hyps dir i hyps =
   let n = List.length hyps in
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 5cd703a25..0f83e16ec 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -23,9 +23,12 @@ 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
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 1889054f8..c1d69dfc5 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -33,9 +33,11 @@ let re_sig it  gc = { it = it; sigma = gc; }
 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"]
 
 let sig_it   = Refiner.sig_it
 let project  = Refiner.project
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index de96f8510..31496fb3d 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -30,9 +30,12 @@ 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
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index dc310c542..2408b8f2b 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -70,11 +70,10 @@ let first_goal gls =
 (* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
 
 let apply_tac_list tac glls =
-  let (sigr,lg) = unpackage glls in
-  match lg with
+  match glls.it with
   | (g1::rest) ->
-      let gl = apply_sig_tac sigr tac g1 in
-      repackage sigr (gl@rest)
+      let pack = tac (re_sig g1 glls.sigma) in
+      re_sig (pack.it @ rest) pack.sigma
   | _ -> user_err Pp.(str "apply_tac_list")
 
 let one_step l gl =