Merge PR #13415: Separate interning and pretyping of universes

Reviewed-by: mattam82

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())