aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssrmatching
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssrmatching')
-rw-r--r--plugins/ssrmatching/ssrmatching.ml8
1 files changed, 6 insertions, 2 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index a4aa08300d..ea014250ca 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -88,8 +88,12 @@ let pr_guarded guard prc c =
let s = Pp.string_of_ppcmds (prc c) ^ "$" in
if guard s (skip_wschars s 0) then pr_paren prc c else prc c
(* More sensible names for constr printers *)
-let prl_glob_constr c = pr_lglob_constr_env (Global.env ()) c
-let pr_glob_constr c = pr_glob_constr_env (Global.env ()) c
+let with_global_env_evm f x =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ f env sigma x
+let prl_glob_constr = with_global_env_evm pr_lglob_constr_env
+let pr_glob_constr = with_global_env_evm pr_glob_constr_env
let prl_constr_expr = pr_lconstr_expr
let pr_constr_expr = pr_constr_expr
let prl_glob_constr_and_expr env sigma = function