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.

7 files changed, 19 insertions, 20 deletions

diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 1705915e70..1987d48e0f 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -109,9 +109,8 @@ let do_universe ~poly l =
 
 let do_constraint ~poly l =
   let open Univ in
-  let u_of_id x =
-    Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x
-  in
+  let evd = Evd.from_env (Global.env ()) in
+  let u_of_id x = Constrintern.interp_known_level evd x in
   let constraints = List.fold_left (fun acc (l, d, r) ->
       let lu = u_of_id l and ru = u_of_id r in
       Constraint.add (lu, d, ru) acc)
diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli
index e4d1d5dc65..ca990a58eb 100644
--- a/vernac/declareUniv.mli
+++ b/vernac/declareUniv.mli
@@ -17,4 +17,4 @@ exception AlreadyDeclared of (string option * Id.t)
 val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
 
 val do_universe : poly:bool -> lident list -> unit
-val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit
+val do_constraint : poly:bool -> Constrexpr.univ_constraint_expr list -> unit
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 9d86ea90e6..f35c77ec3b 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -961,7 +961,7 @@ let explain_not_match_error = function
         status (not b) ++ str" declaration was found"
   | IncompatibleUniverses incon ->
     str"the universe constraints are inconsistent: " ++
-      Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon
+      Univ.explain_universe_inconsistency UnivNames.(pr_with_global_universes empty_binders) incon
   | IncompatiblePolymorphism (env, t1, t2) ->
     str "conversion of polymorphic values generates additional constraints: " ++
       quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t1) ++ spc () ++
@@ -1218,7 +1218,7 @@ let error_large_non_prop_inductive_not_in_type () =
   str "Large non-propositional inductive types must be in Type."
 
 let error_inductive_missing_constraints (us,ind_univ) =
-  let pr_u = Univ.Universe.pr_with UnivNames.pr_with_global_universes in
+  let pr_u = Univ.Universe.pr_with UnivNames.(pr_with_global_universes empty_binders) in
   str "Missing universe constraint declared for inductive type:" ++ spc()
   ++ v 0 (prlist_with_sep spc (fun u ->
       hov 0 (pr_u u ++ str " <= " ++ pr_u ind_univ))
@@ -1406,7 +1406,7 @@ let _ = CErrors.register_handler (wrap_unhandled explain_exn_default)
 let rec vernac_interp_error_handler = function
   | Univ.UniverseInconsistency i ->
     str "Universe inconsistency." ++ spc() ++
-    Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i ++ str "."
+    Univ.explain_universe_inconsistency UnivNames.(pr_with_global_universes empty_binders) i ++ str "."
   | TypeError(ctx,te) ->
     let te = map_ptype_error EConstr.of_constr te in
     explain_type_error ctx Evd.empty te
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 01873918aa..ff4365c8d3 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -60,8 +60,8 @@ let pr_red_expr =
     keyword
 
 let pr_uconstraint (l, d, r) =
-  pr_glob_sort_name l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
-  pr_glob_sort_name r
+  pr_sort_name_expr l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
+  pr_sort_name_expr r
 
 let pr_univ_name_list = function
   | None -> mt ()
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 840754ccc6..0fc6c7f87b 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -206,7 +206,7 @@ let print_if_is_coercion ref =
 
 let pr_template_variables = function
   | [] -> mt ()
-  | vars -> str "on " ++ prlist_with_sep spc UnivNames.pr_with_global_universes vars
+  | vars -> str "on " ++ prlist_with_sep spc UnivNames.(pr_with_global_universes empty_binders) vars
 
 let print_polymorphism ref =
   let poly = Global.is_polymorphic ref in
@@ -668,7 +668,7 @@ let gallina_print_syntactic_def env kn =
         spc () ++ str ":=") ++
      spc () ++
      Constrextern.without_specific_symbols
-       [Notation.SynDefRule kn] (pr_glob_constr_env env) c)
+       [Notation.SynDefRule kn] (pr_glob_constr_env env (Evd.from_env env)) c)
 
 module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> Pp.t option end)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0f63dfe5ce..57b264bbc2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -353,9 +353,9 @@ let universe_subgraph ?loc kept univ =
   let open Univ in
   let sigma = Evd.from_env (Global.env()) in
   let parse q =
-    let q =  Glob_term.(GType q) in
+    let q = Constrexpr.CType q in
     (* this function has a nice error message for not found univs *)
-    Pretyping.interp_known_glob_level ?loc sigma q
+    Constrintern.interp_known_level sigma q
   in
   let kept = List.fold_left (fun kept q -> LSet.add (parse q) kept) LSet.empty kept in
   let csts = UGraph.constraints_for ~kept univ in
@@ -377,7 +377,7 @@ let print_universes ?loc ~sort ~subgraph dst =
     if Global.is_joined_environment () then mt ()
     else str"There may remain asynchronous universe constraints"
   in
-  let prl = UnivNames.pr_with_global_universes in
+  let prl = UnivNames.(pr_with_global_universes empty_binders) in
   begin match dst with
     | None -> UGraph.pr_universes prl univ ++ pr_remaining
     | Some s -> dump_universes_gen (fun u -> Pp.string_of_ppcmds (prl u)) univ s
@@ -1829,11 +1829,11 @@ let vernac_print ~pstate =
   | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s
   | PrintHintDb -> Hints.pr_searchtable env sigma
   | PrintScopes ->
-    Notation.pr_scopes (Constrextern.without_symbols (pr_glob_constr_env env))
+    Notation.pr_scopes (Constrextern.without_symbols (pr_glob_constr_env env sigma))
   | PrintScope s ->
-    Notation.pr_scope (Constrextern.without_symbols (pr_glob_constr_env env)) s
+    Notation.pr_scope (Constrextern.without_symbols (pr_glob_constr_env env sigma)) s
   | PrintVisibility s ->
-    Notation.pr_visibility (Constrextern.without_symbols (pr_glob_constr_env env)) s
+    Notation.pr_visibility (Constrextern.without_symbols (pr_glob_constr_env env sigma)) s
   | PrintAbout (ref_or_by_not,udecl,glnumopt) ->
     print_about_hyp_globs ~pstate ref_or_by_not udecl glnumopt
   | PrintImplicit qid ->
@@ -1867,9 +1867,9 @@ let vernac_locate ~pstate = let open Constrexpr in function
   | LocateTerm {v=AN qid} -> Prettyp.print_located_term qid
   | LocateAny {v=ByNotation (ntn, sc)} (* TODO : handle Ltac notations *)
   | LocateTerm {v=ByNotation (ntn, sc)} ->
-    let _, env = get_current_or_global_context ~pstate in
+    let sigma, env = get_current_or_global_context ~pstate in
     Notation.locate_notation
-      (Constrextern.without_symbols (pr_glob_constr_env env)) ntn sc
+      (Constrextern.without_symbols (pr_glob_constr_env env sigma)) ntn sc
   | LocateLibrary qid -> print_located_library qid
   | LocateModule qid -> Prettyp.print_located_module qid
   | LocateOther (s, qid) -> Prettyp.print_located_other s qid
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 89c09bb169..2e360cf969 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -339,7 +339,7 @@ type nonrec vernac_expr =
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
   | VernacUniverse of lident list
-  | VernacConstraint of Glob_term.glob_constraint list
+  | VernacConstraint of univ_constraint_expr list
 
   (* Gallina extensions *)
   | VernacBeginSection of lident