Separate interning and pretyping of universes

This allows proper treatment in notations, ie fixes #13303

The "glob" representation of universes (what pretyping sees) contains
only fully interpreted (kernel) universes and unbound universe
ids (for non Strict Universe Declaration).

This means universes need to be understood at intern time, so intern
now has a new "universe binders" argument. We cannot avoid this due to
the following example:

~~~coq
Module Import M. Universe i. End M.
Definition foo@{i} := Type@{i}.
~~~

When interning `Type@{i}` we need to know that `i` is locally bound to
avoid interning it as `M.i`.

Extern has a symmetrical problem:

~~~coq
Module Import M. Universe i. End M.
Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
Print foo. (* must not print Type@{i} -> Type@{i} *)
~~~
(Polymorphic as otherwise the local `i` will be called `foo.i`)

Therefore extern also takes a universe binders argument.

Note that the current implementation actually replaces local universes
with names at detype type. (Asymmetrical to pretyping which only gets
names in glob terms for dynamically declared univs, although it's
capable of understanding bound univs too)

As such extern only really needs the domain of the universe
binders (ie the set of bound universe ids), we just arbitrarily pass
the whole universe binders to avoid putting `Id.Map.domain` at every
entry point.

Note that if we want to change so that detyping does not name locally
bound univs we would need to pass the reverse universe binders (map
from levels to ids, contained in the ustate ie in the evar map) to
extern.

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