diff options
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) |