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.

8 files changed, 32 insertions, 32 deletions

diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index ff4a82f864..daed855600 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -150,7 +150,7 @@ let pr_occurrences = pr_occurrences () () ()
 let pr_gen env sigma prc _prlc _prtac x = prc env sigma x
 
 let pr_globc env sigma _prc _prlc _prtac (_,glob) =
-  Printer.pr_glob_constr_env env glob
+  Printer.pr_glob_constr_env env sigma glob
 
 let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t)
 
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index eed9419946..069a342b2a 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -63,7 +63,7 @@ let eval_uconstrs ist cs =
 
 let pr_auto_using_raw env sigma _ _ _  = Pptactic.pr_auto_using @@ Ppconstr.pr_constr_expr env sigma
 let pr_auto_using_glob env sigma _ _ _ = Pptactic.pr_auto_using (fun (c,_) ->
-    Printer.pr_glob_constr_env env c)
+    Printer.pr_glob_constr_env env sigma c)
 let pr_auto_using env sigma _ _ _ = Pptactic.pr_auto_using @@
      Printer.pr_closed_glob_env env sigma
 
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index a3f03b5bb5..f12ca0685e 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -40,9 +40,9 @@ type glob_constr_with_bindings = glob_constr_and_expr with_bindings
 type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings
 
 let pr_glob_constr_with_bindings_sign env sigma _ _ _ (ge : glob_constr_with_bindings_sign) =
-  Printer.pr_glob_constr_env env (fst (fst (snd ge)))
+  Printer.pr_glob_constr_env env sigma (fst (fst (snd ge)))
 let pr_glob_constr_with_bindings env sigma _ _ _ (ge : glob_constr_with_bindings) =
-  Printer.pr_glob_constr_env env (fst (fst ge))
+  Printer.pr_glob_constr_env env sigma (fst (fst ge))
 let pr_constr_expr_with_bindings env sigma prc _ _ (ge : constr_expr_with_bindings) = prc env sigma (fst ge)
 let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c)
 let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index cd7b1f7f28..fa5bbf7676 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1130,12 +1130,12 @@ let pr_goal_selector ~toplevel s =
     let rec prtac n (t:glob_tactic_expr) =
       let pr = {
         pr_tactic = prtac;
-        pr_constr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
-        pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
-        pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env));
-        pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env));
+        pr_constr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma));
+        pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma));
+        pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env sigma));
+        pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env sigma));
         pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env));
-        pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env));
+        pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env sigma));
         pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
         pr_name = pr_lident;
         pr_generic = Pputils.pr_glb_generic;
@@ -1166,7 +1166,7 @@ let pr_goal_selector ~toplevel s =
       let pr = {
         pr_tactic = (fun _ _ -> str "<tactic>");
         pr_constr = pr_econstr_env;
-        pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
+        pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma));
         pr_lconstr = pr_leconstr_env;
         pr_pattern = pr_constr_pattern_env;
         pr_lpattern = pr_lconstr_pattern_env;
@@ -1189,7 +1189,7 @@ let pr_goal_selector ~toplevel s =
 
   let pr_raw_extend env sigma = pr_raw_extend_rec @@ pr_raw_tactic_level env sigma
 
-  let pr_glob_extend env sigma = pr_glob_extend_rec (pr_glob_tactic_level env)
+  let pr_glob_extend env = pr_glob_extend_rec (pr_glob_tactic_level env)
 
   let pr_alias pr lev key args =
     pr_alias_gen (fun _ arg -> pr arg) lev key args
@@ -1212,8 +1212,8 @@ let declare_extra_genarg_pprule wit
         f env sigma pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in
   let g x =
     Genprint.PrinterBasic (fun env sigma ->
-    g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env))
-      (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env))
+    g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma))
+      (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env sigma))
       (fun env sigma -> pr_glob_tactic_level env) x)
   in
   let h x =
@@ -1242,8 +1242,8 @@ let declare_extra_genarg_pprule_with_level wit
         default_already_surrounded = default_surrounded;
         default_ensure_surrounded = default_non_surrounded;
         printer = (fun env sigma n ->
-          g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env))
-            (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env))
+          g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env sigma))
+            (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env sigma))
             (fun env sigma -> pr_glob_tactic_level env) n x) }
   in
   let h x =
@@ -1301,10 +1301,10 @@ let register_basic_print0 wit f g h =
   Genprint.register_print0 wit (lift f) (lift g) (lift_top h)
 
 let pr_glob_constr_pptac env sigma c =
-  pr_glob_constr_env env c
+  pr_glob_constr_env env sigma c
 
 let pr_lglob_constr_pptac env sigma c =
-  pr_lglob_constr_env env c
+  pr_lglob_constr_env env sigma c
 
 let pr_raw_intro_pattern =
   lift_env (fun env sigma -> Miscprint.pr_intro_pattern @@ pr_constr_expr env sigma)
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 5e199dad62..79e0adf9f7 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -124,7 +124,7 @@ val pr_glb_generic : env -> Evd.evar_map -> glevel generic_argument -> Pp.t
 val pr_raw_extend: env -> Evd.evar_map -> int ->
   ml_tactic_entry -> raw_tactic_arg list -> Pp.t
 
-val pr_glob_extend: env -> Evd.evar_map -> int ->
+val pr_glob_extend: env -> int ->
   ml_tactic_entry -> glob_tactic_arg list -> Pp.t
 
 val pr_extend :
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 9c15d24dd3..aa2449d962 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -244,7 +244,8 @@ let string_of_call ck =
          (Pptactic.pr_glob_tactic (Global.env ())
             (Tacexpr.TacAtom (CAst.make te)))
        | Tacexpr.LtacConstrInterp (c, _) ->
-         pr_glob_constr_env (Global.env ()) c
+         let env = Global.env () in
+         pr_glob_constr_env env (Evd.from_env env) c
        | Tacexpr.LtacMLCall te ->
          (Pptactic.pr_glob_tactic (Global.env ())
             te)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 00ac155f0e..f2241e78d2 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -773,7 +773,7 @@ let interp_may_eval f ist env sigma = function
           function already use effect, I call [run] hoping it doesn't mess
           up with any assumption. *)
        Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () ->
-         str"interpretation of term " ++ pr_glob_constr_env env (fst c)));
+         str"interpretation of term " ++ pr_glob_constr_env env sigma (fst c)));
        Exninfo.iraise reraise
 
 (* Interprets a constr expression possibly to first evaluate *)
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 5fbea4eeef..c4c528d373 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -16,11 +16,12 @@ open Tacexpr
 let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
 
 let prtac x =
-  Pptactic.pr_glob_tactic (Global.env()) x
+  let env = Global.env () in
+  Pptactic.pr_glob_tactic env x
 let prmatchpatt env sigma hyp =
   Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp
 let prmatchrl env sigma rl =
-  Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env()))
+  Pptactic.pr_match_rule false prtac
     (fun (_,p) -> Printer.pr_constr_pattern_env env sigma p) rl
 
 (* This module intends to be a beginning of debugger for tactic expressions.
@@ -366,24 +367,22 @@ let explain_ltac_call_trace last trace loc =
     | Tacexpr.LtacNotationCall kn -> quote (Pptactic.pr_alias_key kn)
   | Tacexpr.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
   | Tacexpr.LtacMLCall t ->
-      quote (Pptactic.pr_glob_tactic (Global.env()) t)
+      quote (prtac t)
   | Tacexpr.LtacVarCall (id,t) ->
       quote (Id.print id) ++ strbrk " (bound to " ++
-        Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
+        prtac t ++ str ")"
   | Tacexpr.LtacAtomCall te ->
-      quote (Pptactic.pr_glob_tactic (Global.env())
-              (Tacexpr.TacAtom (CAst.make te)))
+      quote (prtac (Tacexpr.TacAtom (CAst.make te)))
   | Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) ->
-      quote (Printer.pr_glob_constr_env (Global.env()) c) ++
+    (* XXX: This hooks into the CErrors's additional error info API so
+       it is tricky to provide the right env for now. *)
+      let env = Global.env() in
+      let sigma = Evd.from_env env in
+      quote (Printer.pr_glob_constr_env env sigma c) ++
         (if not (Id.Map.is_empty vars) then
           strbrk " (with " ++
             prlist_with_sep pr_comma
             (fun (id,c) ->
-              (* XXX: This hooks into the CErrors's additional error
-                 info API so it is tricky to provide the right env for
-                 now. *)
-              let env = Global.env () in
-              let sigma = Evd.from_env env in
               Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c)
             (List.rev (Id.Map.bindings vars)) ++ str ")"
         else mt())