Merge PR #7859: Remove himsg.pr_puniverses, use @{} for universe printing in errors

6 files changed, 22 insertions, 26 deletions

diff --git a/dev/ci/user-overlays/07859-printers.sh b/dev/ci/user-overlays/07859-printers.sh
new file mode 100644
index 0000000000..27f588e214
--- /dev/null
+++ b/dev/ci/user-overlays/07859-printers.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "7859" ] || [ "$CI_BRANCH" = "rm-univ-broken-printing" ]; then
+    Equations_CI_BRANCH=fix-printers
+    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+fi
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index fd7135b6a6..7258bb9b72 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -98,7 +98,8 @@ let print_ref reduce ref udecl =
       (Array.to_list (Univ.Instance.to_array inst)) udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   let inst =
-    if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs
+    if Global.is_polymorphic ref
+    then Printer.pr_universe_instance sigma (Univ.UContext.instance univs)
     else mt ()
   in
   hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ 
@@ -552,8 +553,7 @@ let print_instance sigma cb =
   if Declareops.constant_is_polymorphic cb then
     let univs = Declareops.constant_polymorphic_context cb in
     let inst = Univ.AUContext.instance univs in
-    let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
-    pr_universe_instance sigma univs
+    pr_universe_instance sigma inst
   else mt()
 				
 let print_constant with_values sep sp udecl =
diff --git a/printing/printer.ml b/printing/printer.ml
index ba094596ff..a77c1ced56 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -290,11 +290,13 @@ let pr_cumulativity_info sigma cumi =
 let pr_global_env = pr_global_env
 let pr_global = pr_global_env Id.Set.empty
 
-let pr_puniverses f env (c,u) =
-  f env c ++ 
-  (if !Constrextern.print_universes then
-    str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
-   else mt ())
+let pr_universe_instance evd inst =
+  str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}"
+
+let pr_puniverses f env sigma (c,u) =
+  if !Constrextern.print_universes
+  then f env c ++ pr_universe_instance sigma u
+  else f env c
 
 let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
 let pr_existential_key = Termops.pr_existential_key
@@ -1016,10 +1018,6 @@ let pr_polymorphic b =
     if b then str"Polymorphic " else str"Monomorphic "
   else mt ()
 
-let pr_universe_instance evd ctx =
-  let inst = Univ.UContext.instance ctx in
-    str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}"
-
 (* print the proof step, possibly with diffs highlighted, *)
 let print_and_diff oldp newp =
   match newp with
diff --git a/printing/printer.mli b/printing/printer.mli
index 948b06f3f6..971241d5f9 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -120,7 +120,7 @@ val pr_sort                : evar_map -> Sorts.t -> Pp.t
 
 val pr_polymorphic         : bool -> Pp.t
 val pr_cumulative          : bool -> bool -> Pp.t
-val pr_universe_instance   : evar_map -> Univ.UContext.t -> Pp.t
+val pr_universe_instance   : evar_map -> Univ.Instance.t -> Pp.t
 val pr_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
   Univ.UContext.t -> Pp.t
 val pr_universe_ctx_set    : evar_map -> Univ.ContextSet.t -> Pp.t
@@ -139,9 +139,9 @@ val pr_constructor         : env -> constructor -> Pp.t
 val pr_inductive           : env -> inductive -> Pp.t
 val pr_evaluable_reference : evaluable_global_reference -> Pp.t
 
-val pr_pconstant           : env -> pconstant -> Pp.t
-val pr_pinductive          : env -> pinductive -> Pp.t
-val pr_pconstructor        : env -> pconstructor -> Pp.t
+val pr_pconstant : env -> evar_map -> pconstant -> Pp.t
+val pr_pinductive : env -> evar_map -> pinductive -> Pp.t
+val pr_pconstructor : env -> evar_map -> pconstructor -> Pp.t
 
 
 (** Contexts *)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 3f95dcfb6d..e2d9850bf8 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -103,9 +103,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
   let envpar = push_rel_context params env in
   let inst =
     if Declareops.inductive_is_polymorphic mib then
-      let ctx = Declareops.inductive_polymorphic_context mib in
-      let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
-      Printer.pr_universe_instance sigma ctx
+      Printer.pr_universe_instance sigma u
     else mt ()
   in
   hov 0 (
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index c49ffe2679..e208d176bb 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -194,12 +194,6 @@ let rec pr_disjunction pr = function
   | a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l
   | [] -> assert false
 
-let pr_puniverses f env (c,u) = 
-  f env c ++ 
-  (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then
-    str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
-  else mt())
-
 let explain_elim_arity env sigma ind sorts c pj okinds =
   let open EConstr in
   let env = make_all_name_different env sigma in
@@ -262,7 +256,7 @@ let explain_ill_formed_branch env sigma c ci actty expty =
   let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in
   strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++
   spc () ++ strbrk "the branch for constructor" ++ spc () ++
-  quote (pr_puniverses pr_constructor env ci) ++
+  quote (pr_pconstructor env sigma ci) ++
   spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++
   str "which should be" ++ brk(1,1) ++ pe ++ str "."