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.

4 files changed, 6 insertions, 3 deletions

diff --git a/library/libnames.ml b/library/libnames.ml
index 88b2e41855..ba1ef1e2f9 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -145,6 +145,8 @@ let qualid_of_dirpath ?loc dir =
   let (l,a) = split_dirpath dir in
   make_qualid ?loc l a
 
+let qualid_of_lident lid = qualid_of_ident ?loc:lid.CAst.loc lid.CAst.v
+
 let qualid_is_ident qid =
   DirPath.is_empty qid.CAst.v.dirpath
 
diff --git a/library/libnames.mli b/library/libnames.mli
index a384510879..65aca0c87d 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -77,6 +77,7 @@ val qualid_of_string : ?loc:Loc.t -> string -> qualid
 val qualid_of_path : ?loc:Loc.t -> full_path -> qualid
 val qualid_of_dirpath : ?loc:Loc.t -> DirPath.t -> qualid
 val qualid_of_ident : ?loc:Loc.t -> Id.t -> qualid
+val qualid_of_lident : lident -> qualid
 
 val qualid_is_ident : qualid -> bool
 val qualid_path : qualid -> DirPath.t
diff --git a/library/nametab.ml b/library/nametab.ml
index a51c281f2b..d5cc4f8ac5 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -562,9 +562,9 @@ let shortest_qualid_of_modtype ?loc kn =
   let sp = MPmap.find kn !the_modtyperevtab in
     MPTab.shortest_qualid ?loc Id.Set.empty sp !the_modtypetab
 
-let shortest_qualid_of_universe ?loc kn =
+let shortest_qualid_of_universe ?loc ctx kn =
   let sp = UnivIdMap.find kn !the_univrevtab in
-    UnivTab.shortest_qualid ?loc Id.Set.empty sp !the_univtab
+    UnivTab.shortest_qualid ?loc ctx sp !the_univtab
 
 let pr_global_env env ref =
   try pr_qualid (shortest_qualid_of_global env ref)
diff --git a/library/nametab.mli b/library/nametab.mli
index 8a8b59733c..fa27dcab9a 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -206,7 +206,7 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
 val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
 val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
-val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid
+val shortest_qualid_of_universe : ?loc:Loc.t -> Id.Set.t -> Univ.Level.UGlobal.t -> qualid
 
 (** {5 Generic name handling} *)