diff options
| author | Emilio Jesus Gallego Arias | 2020-05-11 15:17:35 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-11 15:17:35 +0200 |
| commit | 76f7adccc72e6e85bfc2aaec7c5f348e5966b024 (patch) | |
| tree | ef106b6e627a492313dc0c4516a0f9faee79b01d /plugins/ssr | |
| parent | 0abac9befe6f165dd7829430a229192e6cb18453 (diff) | |
| parent | 1d16c80c53702c3118cc61729a0823d4a9cdaf78 (diff) | |
Merge PR #12273: Deprecate Refiner API
Reviewed-by: ejgallego
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) |