Merge PR #9325: Stop [Print] from saying [is (not) universe polymorphic].

Reviewed-by: maximedenes

14 files changed, 1 insertions, 95 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index c417ef8a66..408bd5f60b 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -267,7 +267,6 @@ let print_name_infos ref =
        print_ref true ref None; blankline]
     else
       [] in
-  print_polymorphism ref @
   print_type_in_type ref @
   print_primitive ref @
   type_info_for_implicit @
@@ -838,6 +837,7 @@ let print_about_any ?loc env sigma k udecl =
     Dumpglob.add_glob ?loc ref;
       pr_infos_list
        (print_ref false ref udecl :: blankline ::
+        print_polymorphism ref @
 	print_name_infos ref @
 	(if Pp.ismt rb then [] else [rb]) @
 	print_opacity ref @
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 583ea0cb43..ba4bc070c6 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -52,7 +52,6 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
-myplus is not universe polymorphic
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
@@ -92,7 +91,6 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
-myplus is not universe polymorphic
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
diff --git a/test-suite/output/Binder.out b/test-suite/output/Binder.out
index 6e27837b26..34558e9a6b 100644
--- a/test-suite/output/Binder.out
+++ b/test-suite/output/Binder.out
@@ -1,12 +1,8 @@
 foo = fun '(x, y) => x + y
      : nat * nat -> nat
-
-foo is not universe polymorphic
 forall '(a, b), a /\ b
      : Prop
 foo = λ '(x, y), x + y
      : nat * nat → nat
-
-foo is not universe polymorphic
 ∀ '(a, b), a ∧ b
      : Prop
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index efcc299e82..cb835ab48d 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -7,7 +7,6 @@ fix F (t : t) : P t :=
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
 
-t_rect is not universe polymorphic
 Argument scopes are [function_scope function_scope _]
      = fun d : TT => match d with
                      | {| f3 := b |} => b
@@ -27,7 +26,6 @@ match Nat.eq_dec x y with
 end
      : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
 
-proj is not universe polymorphic
 Argument scopes are [nat_scope nat_scope function_scope _ _]
 foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
@@ -38,7 +36,6 @@ fix foo (A : Type) (l : list A) {struct l} : option A :=
   end
      : forall A : Type, list A -> option A
 
-foo is not universe polymorphic
 Argument scopes are [type_scope list_scope]
 uncast = 
 fun (A : Type) (x : I A) => match x with
@@ -46,12 +43,9 @@ fun (A : Type) (x : I A) => match x with
                             end
      : forall A : Type, I A -> A
 
-uncast is not universe polymorphic
 Argument scopes are [type_scope _]
 foo' = if A 0 then true else false
      : bool
-
-foo' is not universe polymorphic
 f = 
 fun H : B =>
 match H with
@@ -62,8 +56,6 @@ match H with
      else fun _ : P false => Logic.I) x
 end
      : B -> True
-
-f is not universe polymorphic
 The command has indeed failed with message:
 Non exhaustive pattern-matching: no clause found for pattern 
 gadtTy _ _
@@ -86,19 +78,14 @@ The constructor D (in type J) expects 3 arguments.
 lem1 = 
 fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
      : forall k : nat * nat, k = k
-
-lem1 is not universe polymorphic
 lem2 = 
 fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl
      : forall k : bool, k = k
 
-lem2 is not universe polymorphic
 Argument scope is [bool_scope]
 lem3 = 
 fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
      : forall k : nat * nat, k = k
-
-lem3 is not universe polymorphic
 1 subgoal
   
   x : nat
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 0b0f501f9a..3b65003c29 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -5,7 +5,6 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I
 d2 = fun x : nat => d1 (y:=x)
      : forall x x0 : nat, x0 = x -> x0 = x
 
-d2 is not universe polymorphic
 Arguments x, x0 are implicit
 Argument scopes are [nat_scope nat_scope _]
 map id (1 :: nil)
diff --git a/test-suite/output/Load.out b/test-suite/output/Load.out
index ebbd5d422b..0904d5540b 100644
--- a/test-suite/output/Load.out
+++ b/test-suite/output/Load.out
@@ -1,10 +1,6 @@
 f = 2
      : nat
-
-f is not universe polymorphic
 u = I
      : True
-
-u is not universe polymorphic
 The command has indeed failed with message:
 Files processed by Load cannot leave open proofs.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 71d92482d0..015dac2512 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -232,7 +232,6 @@ fun l : list nat => match l with
                     end
      : list nat -> list nat
 
-foo is not universe polymorphic
 Argument scope is [list_scope]
 Notation
 "'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope
@@ -263,9 +262,5 @@ myfoo01 tt
      : list (list nat)
 amatch = mmatch 0 (with 0 => 1| 1 => 2 end)
      : unit
-
-amatch is not universe polymorphic
 alist = [0; 1; 2]
      : list nat
-
-alist is not universe polymorphic
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index bdbc5a5960..8a6d94c732 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -1,29 +1,20 @@
 swap = fun '(x, y) => (y, x)
      : A * B -> B * A
-
-swap is not universe polymorphic
 fun '(x, y) => (y, x)
      : A * B -> B * A
 forall '(x, y), swap (x, y) = (y, x)
      : Prop
 proj_informative = fun '(exist _ x _) => x : A
      : {x : A | P x} -> A
-
-proj_informative is not universe polymorphic
 foo = fun '(Bar n b tt p) => if b then n + p else n - p
      : Foo -> nat
-
-foo is not universe polymorphic
 baz = 
 fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1
      : Foo -> Foo -> nat
-
-baz is not universe polymorphic
 swap = 
 fun (A B : Type) '(x, y) => (y, x)
      : forall A B : Type, A * B -> B * A
 
-swap is not universe polymorphic
 Arguments A, B are implicit and maximally inserted
 Argument scopes are [type_scope type_scope _]
 fun (A B : Type) '(x, y) => swap (x, y) = (y, x)
@@ -42,8 +33,6 @@ both_z =
 fun pat : nat * nat =>
 let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p)
      : forall pat : nat * nat, F pat
-
-both_z is not universe polymorphic
 fun '(x, y) '(z, t) => swap (x, y) = (z, t)
      : A * B -> B * A -> Prop
 forall '(x, y) '(z, t), swap (x, y) = (z, t)
@@ -53,7 +42,6 @@ fun (pat : nat) '(x, y) => x + y = pat
 f = fun x : nat => x + x
      : nat -> nat
 
-f is not universe polymorphic
 Argument scope is [nat_scope]
 fun x : nat => x + x
      : nat -> nat
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index da1fca7134..ab4172711e 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -46,7 +46,6 @@ fix add (n m : nat) {struct n} : nat :=
   end
      : nat -> nat -> nat
 
-Nat.add is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 Nat.add : nat -> nat -> nat
 
@@ -86,7 +85,6 @@ Argument x is implicit and maximally inserted
 Expands to: Constant PrintInfos.bar
 *** [ bar : foo ]
 
-bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out
index c7e6ef950e..9366113c0c 100644
--- a/test-suite/output/StringSyntax.out
+++ b/test-suite/output/StringSyntax.out
@@ -433,7 +433,6 @@ end
        P "167" ->
        P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
 
-byte_rect is not universe polymorphic
 Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope]
 byte_rec = 
 fun P : byte -> Set => byte_rect P
@@ -608,7 +607,6 @@ fun P : byte -> Set => byte_rect P
        P "167" ->
        P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
 
-byte_rec is not universe polymorphic
 Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope]
 byte_ind = 
 fun (P : byte -> Prop) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") 
@@ -1045,7 +1043,6 @@ end
        P "167" ->
        P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
 
-byte_ind is not universe polymorphic
 Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope]
 "000"
      : byte
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
index 67b65d4b81..f94ed64234 100644
--- a/test-suite/output/TranspModtype.out
+++ b/test-suite/output/TranspModtype.out
@@ -1,15 +1,7 @@
 TrM.A = M.A
      : Set
-
-TrM.A is not universe polymorphic
 OpM.A = M.A
      : Set
-
-OpM.A is not universe polymorphic
 TrM.B = M.B
      : Set
-
-TrM.B is not universe polymorphic
 *** [ OpM.B : Set ]
-
-OpM.B is not universe polymorphic
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 0bd6ade690..a960fe3441 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -9,7 +9,6 @@ fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
      : forall A : Type@{u}, PWrap@{u} A -> A
 (* u |=  *)
 
-punwrap is universe polymorphic
 Argument scopes are [type_scope _]
 Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A }
 
@@ -20,33 +19,26 @@ fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap
      : forall A : Type@{u}, RWrap@{u} A -> A
 (* u |=  *)
 
-runwrap is universe polymorphic
 Argument scopes are [type_scope _]
 Wrap@{u} = fun A : Type@{u} => A
      : Type@{u} -> Type@{u}
 (* u |=  *)
 
-Wrap is universe polymorphic
 Argument scope is [type_scope]
 wrap@{u} = 
 fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
      : forall A : Type@{u}, Wrap@{u} A -> A
 (* u |=  *)
 
-wrap is universe polymorphic
 Arguments A, Wrap are implicit and maximally inserted
 Argument scopes are [type_scope _]
 bar@{u} = nat
      : Wrap@{u} Set
 (* u |= Set < u *)
-
-bar is universe polymorphic
 foo@{u UnivBinders.17 v} = 
 Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
      : Type@{max(u+1,UnivBinders.17+1,v+1)}
 (* u UnivBinders.17 v |=  *)
-
-foo is universe polymorphic
 Type@{i} -> Type@{j}
      : Type@{max(i+1,j+1)}
 (* {j i} |=  *)
@@ -56,8 +48,6 @@ Type@{i} -> Type@{j}
 mono = Type@{mono.u}
      : Type@{mono.u+1}
 (* {mono.u} |=  *)
-
-mono is not universe polymorphic
 mono
      : Type@{mono.u+1}
 Type@{mono.u}
@@ -78,22 +68,16 @@ bobmorane =
 let tt := Type@{UnivBinders.32} in
 let ff := Type@{UnivBinders.34} in tt -> ff
      : Type@{max(UnivBinders.31,UnivBinders.33)}
-
-bobmorane is not universe polymorphic
 The command has indeed failed with message:
 Universe u already bound.
 foo@{E M N} = 
 Type@{M} -> Type@{N} -> Type@{E}
      : Type@{max(E+1,M+1,N+1)}
 (* E M N |=  *)
-
-foo is universe polymorphic
 foo@{u UnivBinders.17 v} = 
 Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
      : Type@{max(u+1,UnivBinders.17+1,v+1)}
 (* u UnivBinders.17 v |=  *)
-
-foo is universe polymorphic
 Inductive Empty@{E} : Type@{E} :=  
 Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
 
@@ -119,26 +103,18 @@ bind_univs.mono =
 Type@{bind_univs.mono.u}
      : Type@{bind_univs.mono.u+1}
 (* {bind_univs.mono.u} |=  *)
-
-bind_univs.mono is not universe polymorphic
 bind_univs.poly@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
-
-bind_univs.poly is universe polymorphic
 insec@{v} = Type@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* v |=  *)
-
-insec is universe polymorphic
 Inductive insecind@{k} : Type@{k+1} :=  inseccstr : Type@{k} -> insecind@{k}
 
 For inseccstr: Argument scope is [type_scope]
 insec@{u v} = Type@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
-
-insec is universe polymorphic
 Inductive insecind@{u k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{u k}
 
@@ -146,29 +122,19 @@ For inseccstr: Argument scope is [type_scope]
 insec2@{u} = Prop
      : Type@{Set+1}
 (* u |=  *)
-
-insec2 is universe polymorphic
 inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
-
-inmod is universe polymorphic
 SomeMod.inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
-
-SomeMod.inmod is universe polymorphic
 inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
-
-inmod is universe polymorphic
 Applied.infunct@{u v} = 
 inmod@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
-
-Applied.infunct is universe polymorphic
 axfoo@{i UnivBinders.56 UnivBinders.57} :
 Type@{UnivBinders.56} -> Type@{i}
 (* i UnivBinders.56 UnivBinders.57 |=  *)
diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out
index 20568f742a..773533a8d3 100644
--- a/test-suite/output/goal_output.out
+++ b/test-suite/output/goal_output.out
@@ -1,11 +1,7 @@
 Nat.t = nat
      : Set
-
-Nat.t is not universe polymorphic
 Nat.t = nat
      : Set
-
-Nat.t is not universe polymorphic
 1 subgoal
   
   ============================
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index f545ca679c..f7ffd1959a 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -4,8 +4,6 @@ fun e : option L => match e with
                     | None => None
                     end
      : option L -> option L
-
-P is not universe polymorphic
 fun n : nat => let y : T n := A n in ?t ?x : T n
      : forall n : nat, T n
 where