diff options
| author | Pierre-Marie Pédrot | 2020-05-06 18:44:32 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-07 17:30:51 +0200 |
| commit | 1d16c80c53702c3118cc61729a0823d4a9cdaf78 (patch) | |
| tree | 188ad2320571de6ed128049f615bd62665a53e11 /plugins/ssr | |
| parent | ffda464321e856e44c7f99e6aab201770781c806 (diff) | |
Deprecate the legacy tacticals from module Refiner.
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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) |