diff options
| author | coqbot-app[bot] | 2020-11-26 11:06:00 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-26 11:06:00 +0000 |
| commit | 0fc82e9651ee1dbc429c9b328b90ad8ad1a3cb14 (patch) | |
| tree | c99091031ad585bf3249ae089e12f44d4e5d83ce /plugins/ssrmatching | |
| parent | 5c7f71a270b265d1ae3f86cb2a29d28f2310edc5 (diff) | |
| parent | 4011a9137fdebe16aa40cb03ba5ce32c09687c69 (diff) | |
Merge PR #13415: Separate interning and pretyping of universes
Reviewed-by: mattam82
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 8 |
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 |