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.

1 files changed, 8 insertions, 3 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index a9438c4aca..4faa12af79 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -27,6 +27,11 @@ let _ = Detyping.print_evar_arguments := true
 let _ = Detyping.print_universes := true
 let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false
 
+let with_env_evm f x =
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
+  f env sigma x
+
 (* std_ppcmds *)
 let pp   x = Pp.pp_with !Topfmt.std_ft x
 
@@ -75,7 +80,7 @@ let ppeconstr x = pp (pr_econstr x)
 let ppconstr_expr x = let sigma,env = get_current_context () in pp (Ppconstr.pr_constr_expr env sigma x)
 let ppsconstr x = ppconstr (Mod_subst.force_constr x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
-let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x))
+let ppglob_constr = (fun x -> pp(with_env_evm pr_lglob_constr_env x))
 let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x))
 let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e)))
 let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
@@ -130,7 +135,7 @@ let rec pr_closure {idents=idents;typed=typed;untyped=untyped} =
 and pr_closed_glob_constr_idmap x =
   pridmap (fun _ -> pr_closed_glob_constr) x
 and pr_closed_glob_constr {closure=closure;term=term} =
-  pr_closure closure ++ (pr_lglob_constr_env Global.(env ())) term
+  pr_closure closure ++ with_env_evm pr_lglob_constr_env term
 
 let ppclosure x = pp (pr_closure x)
 let ppclosedglobconstr x = pp (pr_closed_glob_constr x)
@@ -212,7 +217,7 @@ let pproof p = pp(Proof.pr_proof p)
 let ppuni u = pp(Universe.pr u)
 let ppuni_level u = pp (Level.pr u)
 
-let prlev = UnivNames.pr_with_global_universes
+let prlev = UnivNames.pr_with_global_universes Id.Map.empty
 let ppuniverse_set l = pp (LSet.pr prlev l)
 let ppuniverse_instance l = pp (Instance.pr prlev l)
 let ppuniverse_context l = pp (pr_universe_context prlev l)