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.

6 files changed, 14 insertions, 15 deletions

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