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.

2 files changed, 12 insertions, 12 deletions

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 68530178f8..efe4bfd7f6 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -106,9 +106,9 @@ GRAMMAR EXTEND Gram
     [ [ c = lconstr -> { c } ] ]
   ;
   sort:
-    [ [ "Set"  -> { UNamed [GSet,0] }
-      | "Prop" -> { UNamed [GProp,0] }
-      | "SProp" -> { UNamed [GSProp,0] }
+    [ [ "Set"  -> { UNamed [CSet,0] }
+      | "Prop" -> { UNamed [CProp,0] }
+      | "SProp" -> { UNamed [CSProp,0] }
       | "Type" -> { UAnonymous {rigid=true} }
       | "Type"; "@{"; "_"; "}" -> { UAnonymous {rigid=false} }
       | "Type"; "@{"; u = universe; "}" -> { UNamed u } ] ]
@@ -124,9 +124,9 @@ GRAMMAR EXTEND Gram
       | -> { 0 } ] ]
   ;
   universe_name:
-    [ [ id = global -> { GType id }
-      | "Set"  -> { GSet }
-      | "Prop" -> { GProp } ] ]
+    [ [ id = global -> { CType id }
+      | "Set"  -> { CSet }
+      | "Prop" -> { CProp } ] ]
   ;
   universe_expr:
     [ [ id = universe_name; n = universe_increment -> { (id,n) } ] ]
@@ -282,12 +282,12 @@ GRAMMAR EXTEND Gram
       | -> { None } ] ]
   ;
   universe_level:
-    [ [ "Set" -> { UNamed GSet }
+    [ [ "Set" -> { UNamed CSet }
       (* no parsing SProp as a level *)
-      | "Prop" -> { UNamed GProp }
+      | "Prop" -> { UNamed CProp }
       | "Type" -> { UAnonymous {rigid=true} }
       | "_" -> { UAnonymous {rigid=false} }
-      | id = global -> { UNamed (GType id) } ] ]
+      | id = global -> { UNamed (CType id) } ] ]
   ;
   fix_decls:
     [ [ dcl = fix_decl -> { let (id,_,_,_,_) = dcl.CAst.v in (id,[dcl.CAst.v]) }
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d0ae594db1..7cd73b4c24 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -190,9 +190,9 @@ module Constr :
       [@@deprecated "Deprecated in 8.13; use 'term' instead"]
     val ident : Id.t Entry.t
     val global : qualid Entry.t
-    val universe_name : Glob_term.glob_sort_name Entry.t
-    val universe_level : Glob_term.glob_level Entry.t
-    val sort : Glob_term.glob_sort Entry.t
+    val universe_name : sort_name_expr Entry.t
+    val universe_level : univ_level_expr Entry.t
+    val sort : sort_expr Entry.t
     val sort_family : Sorts.family Entry.t
     val pattern : cases_pattern_expr Entry.t
     val constr_pattern : constr_expr Entry.t