From 5b432bf03f623b144871181446c68479482abe32 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 26 Apr 2018 14:44:30 +0200
Subject: Deprecate Refiner [evar_map ref] exported functions.

Uses internal to Refiner remain.
---
 plugins/ssr/ssrfwd.ml       | 4 +---
 plugins/ssr/ssrtacticals.ml | 5 ++---
 2 files changed, 3 insertions(+), 6 deletions(-)

(limited to 'plugins/ssr')

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
-- 
cgit v1.2.3