Merge PR #13415: Separate interning and pretyping of universes

Reviewed-by: mattam82

17 files changed, 68 insertions, 67 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index c485c38009..23a7b89d2c 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -443,7 +443,7 @@ let cc_tactic depth additionnal_terms =
       let pr_missing (c, missing) =
         let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
         let holes = List.init missing (fun _ -> hole) in
-        Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
+        Printer.pr_glob_constr_env env sigma (DAst.make @@ GApp (c, holes))
       in
             let msg = Pp.(str "Goal is solvable by congruence but some arguments are missing."
                     ++ fnl () ++
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 767a9ec39b..5bfb37f4cb 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -458,9 +458,11 @@ let rec pattern_to_term_and_type env typ =
    but only the value of the function
 *)
 
+let pr_glob_constr_env env x = pr_glob_constr_env env (Evd.from_env env) x
+
 let rec build_entry_lc env sigma funnames avoid rt :
     glob_constr build_entry_return =
-  observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt);
+  observe (str " Entering : " ++ pr_glob_constr_env env rt);
   let open CAst in
   match DAst.get rt with
   | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _
@@ -638,9 +640,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
       with Not_found ->
         user_err
           ( str "Cannot find the inductive associated to "
-          ++ Printer.pr_glob_constr_env env b
-          ++ str " in "
-          ++ Printer.pr_glob_constr_env env rt
+          ++ pr_glob_constr_env env b ++ str " in " ++ pr_glob_constr_env env rt
           ++ str ". try again with a cast" )
     in
     let case_pats = build_constructors_of_type (fst ind) [] in
@@ -662,9 +662,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
       with Not_found ->
         user_err
           ( str "Cannot find the inductive associated to "
-          ++ Printer.pr_glob_constr_env env b
-          ++ str " in "
-          ++ Printer.pr_glob_constr_env env rt
+          ++ pr_glob_constr_env env b ++ str " in " ++ pr_glob_constr_env env rt
           ++ str ". try again with a cast" )
     in
     let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
@@ -1321,11 +1319,11 @@ let do_build_inductive evd (funconstants : pconstant list)
             @@ Constrexpr.CLetIn
                  ( CAst.make n
                  , with_full_print
-                     (Constrextern.extern_glob_constr Id.Set.empty)
+                     Constrextern.(extern_glob_constr empty_extern_env)
                      t
                  , Some
                      (with_full_print
-                        (Constrextern.extern_glob_constr Id.Set.empty)
+                        Constrextern.(extern_glob_constr empty_extern_env)
                         typ)
                  , acc )
           | None ->
@@ -1335,7 +1333,7 @@ let do_build_inductive evd (funconstants : pconstant list)
                        ( [CAst.make n]
                        , Constrexpr_ops.default_binder_kind
                        , with_full_print
-                           (Constrextern.extern_glob_constr Id.Set.empty)
+                           Constrextern.(extern_glob_constr empty_extern_env)
                            t ) ]
                  , acc ))
         rel_first_args
@@ -1410,11 +1408,11 @@ let do_build_inductive evd (funconstants : pconstant list)
           @@ Constrexpr.CLetIn
                ( CAst.make n
                , with_full_print
-                   (Constrextern.extern_glob_constr Id.Set.empty)
+                   Constrextern.(extern_glob_constr empty_extern_env)
                    t
                , Some
                    (with_full_print
-                      (Constrextern.extern_glob_constr Id.Set.empty)
+                      Constrextern.(extern_glob_constr empty_extern_env)
                       typ)
                , acc )
         | None ->
@@ -1424,7 +1422,7 @@ let do_build_inductive evd (funconstants : pconstant list)
                      ( [CAst.make n]
                      , Constrexpr_ops.default_binder_kind
                      , with_full_print
-                         (Constrextern.extern_glob_constr Id.Set.empty)
+                         Constrextern.(extern_glob_constr empty_extern_env)
                          t ) ]
                , acc ))
       rel_first_args
@@ -1448,16 +1446,16 @@ let do_build_inductive evd (funconstants : pconstant list)
         | Some typ ->
           Constrexpr.CLocalDef
             ( CAst.make n
-            , Constrextern.extern_glob_constr Id.Set.empty t
+            , Constrextern.(extern_glob_constr empty_extern_env) t
             , Some
                 (with_full_print
-                   (Constrextern.extern_glob_constr Id.Set.empty)
+                   Constrextern.(extern_glob_constr empty_extern_env)
                    typ) )
         | None ->
           Constrexpr.CLocalAssum
             ( [CAst.make n]
             , Constrexpr_ops.default_binder_kind
-            , Constrextern.extern_glob_constr Id.Set.empty t ))
+            , Constrextern.(extern_glob_constr empty_extern_env) t ))
       rels_params
   in
   let ext_rels_constructors =
@@ -1466,7 +1464,7 @@ let do_build_inductive evd (funconstants : pconstant list)
            ( false
            , ( CAst.make id
              , with_full_print
-                 (Constrextern.extern_glob_type Id.Set.empty)
+                 Constrextern.(extern_glob_type empty_extern_env)
                  ((* zeta_normalize *) alpha_rt rel_params_ids t) ) )))
       rel_constructors
   in
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index ff4a82f864..daed855600 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -150,7 +150,7 @@ let pr_occurrences = pr_occurrences () () ()
 let pr_gen env sigma prc _prlc _prtac x = prc env sigma x
 
 let pr_globc env sigma _prc _prlc _prtac (_,glob) =
-  Printer.pr_glob_constr_env env glob
+  Printer.pr_glob_constr_env env sigma glob
 
 let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t)
 
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index eed9419946..069a342b2a 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -63,7 +63,7 @@ let eval_uconstrs ist cs =
 
 let pr_auto_using_raw env sigma _ _ _  = Pptactic.pr_auto_using @@ Ppconstr.pr_constr_expr env sigma
 let pr_auto_using_glob env sigma _ _ _ = Pptactic.pr_auto_using (fun (c,_) ->
-    Printer.pr_glob_constr_env env c)
+    Printer.pr_glob_constr_env env sigma c)
 let pr_auto_using env sigma _ _ _ = Pptactic.pr_auto_using @@
      Printer.pr_closed_glob_env env sigma
 
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index a3f03b5bb5..f12ca0685e 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -40,9 +40,9 @@ type glob_constr_with_bindings = glob_constr_and_expr with_bindings
 type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings
 
 let pr_glob_constr_with_bindings_sign env sigma _ _ _ (ge : glob_constr_with_bindings_sign) =
-  Printer.pr_glob_constr_env env (fst (fst (snd ge)))
+  Printer.pr_glob_constr_env env sigma (fst (fst (snd ge)))
 let pr_glob_constr_with_bindings env sigma _ _ _ (ge : glob_constr_with_bindings) =
-  Printer.pr_glob_constr_env env (fst (fst ge))
+  Printer.pr_glob_constr_env env sigma (fst (fst ge))
 let pr_constr_expr_with_bindings env sigma prc _ _ (ge : constr_expr_with_bindings) = prc env sigma (fst ge)
 let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c)
 let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index cd7b1f7f28..fa5bbf7676 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1130,12 +1130,12 @@ let pr_goal_selector ~toplevel s =
     let rec prtac n (t:glob_tactic_expr) =
       let pr = {
         pr_tactic = prtac;
-        pr_constr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
-        pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
-        pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env));
-        pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env));
+        pr_constr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma));
+        pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma));
+        pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env sigma));
+        pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env sigma));
         pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env));
-        pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env));
+        pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env sigma));
         pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
         pr_name = pr_lident;
         pr_generic = Pputils.pr_glb_generic;
@@ -1166,7 +1166,7 @@ let pr_goal_selector ~toplevel s =
       let pr = {
         pr_tactic = (fun _ _ -> str "<tactic>");
         pr_constr = pr_econstr_env;
-        pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
+        pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma));
         pr_lconstr = pr_leconstr_env;
         pr_pattern = pr_constr_pattern_env;
         pr_lpattern = pr_lconstr_pattern_env;
@@ -1189,7 +1189,7 @@ let pr_goal_selector ~toplevel s =
 
   let pr_raw_extend env sigma = pr_raw_extend_rec @@ pr_raw_tactic_level env sigma
 
-  let pr_glob_extend env sigma = pr_glob_extend_rec (pr_glob_tactic_level env)
+  let pr_glob_extend env = pr_glob_extend_rec (pr_glob_tactic_level env)
 
   let pr_alias pr lev key args =
     pr_alias_gen (fun _ arg -> pr arg) lev key args
@@ -1212,8 +1212,8 @@ let declare_extra_genarg_pprule wit
         f env sigma pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in
   let g x =
     Genprint.PrinterBasic (fun env sigma ->
-    g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env))
-      (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env))
+    g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma))
+      (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env sigma))
       (fun env sigma -> pr_glob_tactic_level env) x)
   in
   let h x =
@@ -1242,8 +1242,8 @@ let declare_extra_genarg_pprule_with_level wit
         default_already_surrounded = default_surrounded;
         default_ensure_surrounded = default_non_surrounded;
         printer = (fun env sigma n ->
-          g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env))
-            (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env))
+          g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma))
+            (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env sigma))
             (fun env sigma -> pr_glob_tactic_level env) n x) }
   in
   let h x =
@@ -1301,10 +1301,10 @@ let register_basic_print0 wit f g h =
   Genprint.register_print0 wit (lift f) (lift g) (lift_top h)
 
 let pr_glob_constr_pptac env sigma c =
-  pr_glob_constr_env env c
+  pr_glob_constr_env env sigma c
 
 let pr_lglob_constr_pptac env sigma c =
-  pr_lglob_constr_env env c
+  pr_lglob_constr_env env sigma c
 
 let pr_raw_intro_pattern =
   lift_env (fun env sigma -> Miscprint.pr_intro_pattern @@ pr_constr_expr env sigma)
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 5e199dad62..79e0adf9f7 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -124,7 +124,7 @@ val pr_glb_generic : env -> Evd.evar_map -> glevel generic_argument -> Pp.t
 val pr_raw_extend: env -> Evd.evar_map -> int ->
   ml_tactic_entry -> raw_tactic_arg list -> Pp.t
 
-val pr_glob_extend: env -> Evd.evar_map -> int ->
+val pr_glob_extend: env -> int ->
   ml_tactic_entry -> glob_tactic_arg list -> Pp.t
 
 val pr_extend :
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 9c15d24dd3..aa2449d962 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -244,7 +244,8 @@ let string_of_call ck =
          (Pptactic.pr_glob_tactic (Global.env ())
             (Tacexpr.TacAtom (CAst.make te)))
        | Tacexpr.LtacConstrInterp (c, _) ->
-         pr_glob_constr_env (Global.env ()) c
+         let env = Global.env () in
+         pr_glob_constr_env env (Evd.from_env env) c
        | Tacexpr.LtacMLCall te ->
          (Pptactic.pr_glob_tactic (Global.env ())
             te)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 00ac155f0e..f2241e78d2 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -773,7 +773,7 @@ let interp_may_eval f ist env sigma = function
           function already use effect, I call [run] hoping it doesn't mess
           up with any assumption. *)
        Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () ->
-         str"interpretation of term " ++ pr_glob_constr_env env (fst c)));
+         str"interpretation of term " ++ pr_glob_constr_env env sigma (fst c)));
        Exninfo.iraise reraise
 
 (* Interprets a constr expression possibly to first evaluate *)
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 5fbea4eeef..c4c528d373 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -16,11 +16,12 @@ open Tacexpr
 let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
 
 let prtac x =
-  Pptactic.pr_glob_tactic (Global.env()) x
+  let env = Global.env () in
+  Pptactic.pr_glob_tactic env x
 let prmatchpatt env sigma hyp =
   Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp
 let prmatchrl env sigma rl =
-  Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env()))
+  Pptactic.pr_match_rule false prtac
     (fun (_,p) -> Printer.pr_constr_pattern_env env sigma p) rl
 
 (* This module intends to be a beginning of debugger for tactic expressions.
@@ -366,24 +367,22 @@ let explain_ltac_call_trace last trace loc =
     | Tacexpr.LtacNotationCall kn -> quote (Pptactic.pr_alias_key kn)
   | Tacexpr.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
   | Tacexpr.LtacMLCall t ->
-      quote (Pptactic.pr_glob_tactic (Global.env()) t)
+      quote (prtac t)
   | Tacexpr.LtacVarCall (id,t) ->
       quote (Id.print id) ++ strbrk " (bound to " ++
-        Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
+        prtac t ++ str ")"
   | Tacexpr.LtacAtomCall te ->
-      quote (Pptactic.pr_glob_tactic (Global.env())
-              (Tacexpr.TacAtom (CAst.make te)))
+      quote (prtac (Tacexpr.TacAtom (CAst.make te)))
   | Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) ->
-      quote (Printer.pr_glob_constr_env (Global.env()) c) ++
+    (* XXX: This hooks into the CErrors's additional error info API so
+       it is tricky to provide the right env for now. *)
+      let env = Global.env() in
+      let sigma = Evd.from_env env in
+      quote (Printer.pr_glob_constr_env env sigma c) ++
         (if not (Id.Map.is_empty vars) then
           strbrk " (with " ++
             prlist_with_sep pr_comma
             (fun (id,c) ->
-              (* XXX: This hooks into the CErrors's additional error
-                 info API so it is tricky to provide the right env for
-                 now. *)
-              let env = Global.env () in
-              let sigma = Evd.from_env env in
               Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c)
             (List.rev (Id.Map.bindings vars)) ++ str ")"
         else mt())
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 42b9248979..61643c2aa3 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -50,7 +50,7 @@ let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) =
         SsrHyp (Loc.tag ?loc id) :: clr', rcs'
     | _ -> clr', rcs'
 
-let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl)
+let pf_pr_glob_constr gl = pr_glob_constr_env (pf_env gl) (project gl)
 
 let interp_nbargs ist gl rc =
   try
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index cb58b9bcb8..cd219838d5 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -895,7 +895,7 @@ open Constrexpr
 open Util
 
 (** Constructors for constr_expr *)
-let mkCProp loc = CAst.make ?loc @@ CSort (UNamed [GProp,0])
+let mkCProp loc = CAst.make ?loc @@ CSort (UNamed [CProp,0])
 let mkCType loc = CAst.make ?loc @@ CSort (UAnonymous {rigid=true})
 let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)
 let rec mkCHoles ?loc n =
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index a7ebd5f9f5..fdfba48024 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -84,7 +84,7 @@ let interp_congrarg_at ist gl n rf ty m =
     if i + n > m then None else
     try
       let rt = mkRApp congrn (args1 @  mkRApp rf (mkRHoles i) :: args2) in
-      ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) rt));
+      ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) (project gl) rt));
       Some (interp_refine ist gl rt)
     with _ -> loop (i + 1) in
   loop 0
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index ab36d4fc7c..95c8024e89 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -57,17 +57,16 @@ let pr_guarded guard prc c =
   let s = Format.flush_str_formatter () ^ "$" in
   if guard s (skip_wschars s 0) then pr_paren prc c else prc c
 
-let prl_constr_expr =
+let with_global_env_evm f x =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  Ppconstr.pr_lconstr_expr env sigma
-let pr_glob_constr c = Printer.pr_glob_constr_env (Global.env ()) c
-let prl_glob_constr c = Printer.pr_lglob_constr_env (Global.env ()) c
+  f env sigma x
+
+let prl_constr_expr = with_global_env_evm Ppconstr.pr_lconstr_expr
+let pr_glob_constr = with_global_env_evm Printer.pr_glob_constr_env
+let prl_glob_constr = with_global_env_evm Printer.pr_lglob_constr_env
 let pr_glob_constr_and_expr = function
-  | _, Some c ->
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
-    Ppconstr.pr_constr_expr env sigma c
+  | _, Some c -> with_global_env_evm Ppconstr.pr_constr_expr c
   | c, None -> pr_glob_constr c
 let pr_term (k, c) = pr_guarded (guard_term k) pr_glob_constr_and_expr c
 
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 99cf197b78..3e44bd4d3b 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -203,8 +203,8 @@ let pr_raw_ssrhintref env sigma prc _ _ = let open CAst in function
 let pr_rawhintref env sigma c =
   match DAst.get c with
   | GApp (f, args) when isRHoles args ->
-    pr_glob_constr_env env f ++ str "|" ++ int (List.length args)
-  | _ -> pr_glob_constr_env env c
+    pr_glob_constr_env env sigma f ++ str "|" ++ int (List.length args)
+  | _ -> pr_glob_constr_env env sigma c
 
 let pr_glob_ssrhintref env sigma _ _ _ (c, _) = pr_rawhintref env sigma c
 
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index d99ead139d..97926753f5 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -195,7 +195,7 @@ let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
   let env = Goal.env goal in
   let sigma = Goal.sigma goal in
   Ssrprinters.ppdebug (lazy
-    Pp.(str"interp-in: " ++ Printer.pr_glob_constr_env env glob));
+    Pp.(str"interp-in: " ++ Printer.pr_glob_constr_env env sigma glob));
   try
     let sigma,term = Tacinterp.interp_open_constr ist env sigma (glob,None) in
     Ssrprinters.ppdebug (lazy
@@ -205,7 +205,7 @@ let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
     (* XXX this is another catch all! *)
     let e, info = Exninfo.capture e in
     Ssrprinters.ppdebug (lazy
-    Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env glob));
+    Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env sigma glob));
     tclZERO ~info e
 end
 
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