From 1d16c80c53702c3118cc61729a0823d4a9cdaf78 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 May 2020 18:44:32 +0200
Subject: Deprecate the legacy tacticals from module Refiner.

---
 plugins/ssr/ssrcommon.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index e05c4c26dd..e8257b5dba 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -22,7 +22,7 @@ open Locusops
 
 open Ltac_plugin
 open Tacmach
-open Refiner
+open Tacticals
 open Libnames
 open Ssrmatching_plugin
 open Ssrmatching
@@ -81,6 +81,9 @@ let nohint = false, []
 
 type 'a tac_a = (goal * 'a) sigma -> (goal * 'a) list sigma
 
+let project gl = gl.Evd.sigma
+let re_sig it sigma = { Evd.it = it; Evd.sigma = sigma }
+
 let push_ctx  a gl = re_sig (sig_it gl, a) (project gl)
 let push_ctxs a gl =
   re_sig (List.map (fun x -> x,a) (sig_it gl)) (project gl)
-- 
cgit v1.2.3