Remove is_universe_polymorphism from printing

18 files changed, 171 insertions, 76 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 4619e049e0..37913edc23 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -227,13 +227,11 @@ let print_if_is_coercion ref =
 let print_polymorphism ref =
   let poly = Global.is_polymorphic ref in
   let template_poly = Global.is_template_polymorphic ref in
-  if Flags.is_universe_polymorphism () || poly || template_poly then
-    [ pr_global ref ++ str " is " ++ str
+  [ pr_global ref ++ str " is " ++ str
       (if poly then "universe polymorphic"
        else if template_poly then
 	 "template universe polymorphic"
        else "not universe polymorphic") ]
-  else []
 
 let print_type_in_type ref =
   let unsafe = Global.is_type_in_type ref in
diff --git a/printing/printer.ml b/printing/printer.ml
index 3cf995a005..da364c8b9e 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -969,19 +969,13 @@ let pr_assumptionset env sigma s =
     ] in
     prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
 
-let xor a b = 
-  (a && not b) || (not a && b)
-
 let pr_cumulative poly cum =
   if poly then
     if cum then str "Cumulative " else str "NonCumulative "
   else mt ()
 
 let pr_polymorphic b = 
-  let print = xor (Flags.is_universe_polymorphism ()) b in
-  if print then
-    if b then str"Polymorphic " else str"Monomorphic "
-  else mt ()
+  if b then str"Polymorphic " else str"Monomorphic "
 
 (* print the proof step, possibly with diffs highlighted, *)
 let print_and_diff oldp newp =
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index d587d1f09b..7074ad2d41 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -1,11 +1,13 @@
 Nat.sub : nat -> nat -> nat
 
+Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub but avoid exposing match constructs
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
+Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub when applied to 1 argument
   but avoid exposing match constructs
@@ -13,6 +15,7 @@ Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
+Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub
   when the 1st argument evaluates to a constructor and
@@ -21,6 +24,7 @@ Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
+Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor and when applied to 2 arguments 
@@ -28,6 +32,7 @@ Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
+Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor 
@@ -37,6 +42,7 @@ pf :
 forall D1 C1 : Type,
 (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
 
+pf is not universe polymorphic
 Arguments D2, C2 are implicit
 Arguments D1, C1 are implicit and maximally inserted
 Argument scopes are [foo_scope type_scope _ _ _ _ _]
@@ -45,6 +51,7 @@ pf is transparent
 Expands to: Constant Arguments.pf
 fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
 
+fcomp is not universe polymorphic
 Arguments A, B, C are implicit and maximally inserted
 Argument scopes are [type_scope type_scope type_scope _ _ _]
 The reduction tactics unfold fcomp when applied to 6 arguments 
@@ -52,17 +59,20 @@ fcomp is transparent
 Expands to: Constant Arguments.fcomp
 volatile : nat -> nat
 
+volatile is not universe polymorphic
 Argument scope is [nat_scope]
 The reduction tactics always unfold volatile
 volatile is transparent
 Expands to: Constant Arguments.volatile
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
+f is not universe polymorphic
 Argument scopes are [_ _ nat_scope _ nat_scope]
 f is transparent
 Expands to: Constant Arguments.S1.S2.f
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
+f is not universe polymorphic
 Argument scopes are [_ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 3rd, 4th and
   5th arguments evaluate to a constructor 
@@ -70,6 +80,7 @@ f is transparent
 Expands to: Constant Arguments.S1.S2.f
 f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
+f is not universe polymorphic
 Argument T2 is implicit
 Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 4th, 5th and
@@ -78,6 +89,7 @@ f is transparent
 Expands to: Constant Arguments.S1.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
+f is not universe polymorphic
 Arguments T1, T2 are implicit
 Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 5th, 6th and
@@ -90,6 +102,7 @@ Expands to: Constant Arguments.f
      : Prop
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
+f is not universe polymorphic
 The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor 
 f is transparent
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index febe160820..69ba329ff1 100644
--- a/test-suite/output/ArgumentsScope.out
+++ b/test-suite/output/ArgumentsScope.out
@@ -1,56 +1,70 @@
 a : bool -> bool
 
+a is not universe polymorphic
 Argument scope is [bool_scope]
 Expands to: Variable a
 b : bool -> bool
 
+b is not universe polymorphic
 Argument scope is [bool_scope]
 Expands to: Variable b
 negb'' : bool -> bool
 
+negb'' is not universe polymorphic
 Argument scope is [bool_scope]
 negb'' is transparent
 Expands to: Constant ArgumentsScope.A.B.negb''
 negb' : bool -> bool
 
+negb' is not universe polymorphic
 Argument scope is [bool_scope]
 negb' is transparent
 Expands to: Constant ArgumentsScope.A.negb'
 negb : bool -> bool
 
+negb is not universe polymorphic
 Argument scope is [bool_scope]
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
 a : bool -> bool
 
+a is not universe polymorphic
 Expands to: Variable a
 b : bool -> bool
 
+b is not universe polymorphic
 Expands to: Variable b
 negb : bool -> bool
 
+negb is not universe polymorphic
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
 negb' : bool -> bool
 
+negb' is not universe polymorphic
 negb' is transparent
 Expands to: Constant ArgumentsScope.A.negb'
 negb'' : bool -> bool
 
+negb'' is not universe polymorphic
 negb'' is transparent
 Expands to: Constant ArgumentsScope.A.B.negb''
 a : bool -> bool
 
+a is not universe polymorphic
 Expands to: Variable a
 negb : bool -> bool
 
+negb is not universe polymorphic
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
 negb' : bool -> bool
 
+negb' is not universe polymorphic
 negb' is transparent
 Expands to: Constant ArgumentsScope.negb'
 negb'' : bool -> bool
 
+negb'' is not universe polymorphic
 negb'' is transparent
 Expands to: Constant ArgumentsScope.negb''
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 1755886967..b071da86c9 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -11,7 +11,7 @@ eq_refl
      : ?y = ?y
 where
 ?y : [ |- nat]
-Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 For eq_refl: Arguments are renamed to B, y
 For eq: Argument A is implicit and maximally inserted
@@ -23,6 +23,7 @@ For eq: Argument scopes are [type_scope _ _]
 For eq_refl: Argument scopes are [type_scope _]
 eq_refl : forall (A : Type) (x : A), x = x
 
+eq_refl is not universe polymorphic
 Arguments are renamed to B, y
 When applied to no arguments:
   Arguments B, y are implicit and maximally inserted
@@ -30,7 +31,8 @@ When applied to 1 argument:
   Argument B is implicit
 Argument scopes are [type_scope _]
 Expands to: Constructor Coq.Init.Logic.eq_refl
-Inductive myEq (B : Type) (x : A) : A -> Prop :=  myrefl : B -> myEq B x x
+Monomorphic Inductive myEq (B : Type) (x : A) : A -> Prop :=
+    myrefl : B -> myEq B x x
 
 For myrefl: Arguments are renamed to C, x, _
 For myrefl: Argument C is implicit and maximally inserted
@@ -38,11 +40,12 @@ For myEq: Argument scopes are [type_scope _ _]
 For myrefl: Argument scopes are [type_scope _ _]
 myrefl : forall (B : Type) (x : A), B -> myEq B x x
 
+myrefl is not universe polymorphic
 Arguments are renamed to C, x, _
 Argument C is implicit and maximally inserted
 Argument scopes are [type_scope _ _]
 Expands to: Constructor Arguments_renaming.Test1.myrefl
-myplus = 
+Monomorphic myplus = 
 fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   match n with
   | 0 => m
@@ -50,11 +53,13 @@ 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]
 myplus : 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]
@@ -64,7 +69,7 @@ myplus is transparent
 Expands to: Constant Arguments_renaming.Test1.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
-Inductive myEq (A B : Type) (x : A) : A -> Prop :=
+Monomorphic Inductive myEq (A B : Type) (x : A) : A -> Prop :=
     myrefl : B -> myEq A B x x
 
 For myrefl: Arguments are renamed to A, C, x, _
@@ -73,13 +78,14 @@ For myEq: Argument scopes are [type_scope type_scope _ _]
 For myrefl: Argument scopes are [type_scope type_scope _ _]
 myrefl : forall (A B : Type) (x : A), B -> myEq A B x x
 
+myrefl is not universe polymorphic
 Arguments are renamed to A, C, x, _
 Argument C is implicit and maximally inserted
 Argument scopes are [type_scope type_scope _ _]
 Expands to: Constructor Arguments_renaming.myrefl
 myrefl
      : forall (A C : Type) (x : A), C -> myEq A C x x
-myplus = 
+Monomorphic myplus = 
 fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   match n with
   | 0 => m
@@ -87,11 +93,13 @@ 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]
 myplus : 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 34558e9a6b..9c46ace463 100644
--- a/test-suite/output/Binder.out
+++ b/test-suite/output/Binder.out
@@ -1,8 +1,12 @@
-foo = fun '(x, y) => x + y
+Monomorphic 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
+Monomorphic 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 cb835ab48d..0a02c5a7dd 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -1,4 +1,4 @@
-t_rect = 
+Monomorphic t_rect = 
 fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
 fix F (t : t) : P t :=
   match t as t0 return (P t0) with
@@ -7,6 +7,7 @@ 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
@@ -16,7 +17,7 @@ Argument scopes are [function_scope function_scope _]
                      | {| f3 := b |} => b
                      end
      : TT -> 0 = 0
-proj = 
+Monomorphic proj = 
 fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) =>
 match Nat.eq_dec x y with
 | left eqprf => match eqprf in (_ = z) return (P z) with
@@ -26,8 +27,9 @@ 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 = 
+Monomorphic foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
   match l with
   | nil => None
@@ -36,17 +38,21 @@ 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 = 
+Monomorphic uncast = 
 fun (A : Type) (x : I A) => match x with
                             | x0 <: _ => x0
                             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
+Monomorphic foo' = if A 0 then true else false
      : bool
-f = 
+
+foo' is not universe polymorphic
+Monomorphic f = 
 fun H : B =>
 match H with
 | AC x =>
@@ -56,6 +62,8 @@ 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 _ _
@@ -75,17 +83,22 @@ fun '(D n m p q) => n + m + p + q
      : J -> nat
 The command has indeed failed with message:
 The constructor D (in type J) expects 3 arguments.
-lem1 = 
+Monomorphic lem1 = 
 fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
      : forall k : nat * nat, k = k
-lem2 = 
+
+lem1 is not universe polymorphic
+Monomorphic 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 = 
+Monomorphic 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 3b65003c29..71c7070f2b 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -2,9 +2,11 @@ compose (C:=nat) S
      : (nat -> nat) -> nat -> nat
 ex_intro (P:=fun _ : nat => True) (x:=0) I
      : ex (fun _ : nat => True)
-d2 = fun x : nat => d1 (y:=x)
+Monomorphic 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/Inductive.out b/test-suite/output/Inductive.out
index af202ea01c..6d65db9e22 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -1,7 +1,8 @@
 The command has indeed failed with message:
 Last occurrence of "list'" must have "A" as 1st argument in
  "A -> list' A -> list' (A * A)%type".
-Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
+Monomorphic Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=
+    Foo : foo A x
 
 For foo: Argument scopes are [type_scope _]
 For Foo: Argument scopes are [type_scope _]
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index c17c63e724..4743fb0d0a 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -1,4 +1,4 @@
-Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
+Monomorphic Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
     exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x}
 
 For sig2: Argument A is implicit
diff --git a/test-suite/output/Load.out b/test-suite/output/Load.out
index 0904d5540b..f84cedfa62 100644
--- a/test-suite/output/Load.out
+++ b/test-suite/output/Load.out
@@ -1,6 +1,10 @@
-f = 2
+Monomorphic f = 2
      : nat
-u = I
+
+f is not universe polymorphic
+Monomorphic 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 d32cf67e28..48379f713d 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -223,13 +223,14 @@ fun S : nat => [[S | S.S]]
      : Set
 exists2 '{{y, z}} : nat * nat, y > z & z > y
      : Prop
-foo = 
+Monomorphic foo = 
 fun l : list nat => match l with
                     | _ :: (_ :: _) as l1 => l1
                     | _ => l
                     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
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index 8a6d94c732..bfeff20524 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -1,20 +1,31 @@
-swap = fun '(x, y) => (y, x)
+Monomorphic 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
+Monomorphic proj_informative = 
+fun '(exist _ x _) => x : A
      : {x : A | P x} -> A
-foo = fun '(Bar n b tt p) => if b then n + p else n - p
+
+proj_informative is not universe polymorphic
+Monomorphic foo = 
+fun '(Bar n b tt p) => if b then n + p else n - p
      : Foo -> nat
-baz = 
+
+foo is not universe polymorphic
+Monomorphic baz = 
 fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1
      : Foo -> Foo -> nat
-swap = 
+
+baz is not universe polymorphic
+Monomorphic 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)
@@ -29,19 +40,22 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w)
      : A * B → B * A
 ∀ '(x, y), swap (x, y) = (y, x)
      : Prop
-both_z = 
+Monomorphic 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)
      : Prop
 fun (pat : nat) '(x, y) => x + y = pat
      : nat -> nat * nat -> Prop
-f = fun x : nat => x + x
+Monomorphic 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 38a16e01c2..be793dd453 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -4,7 +4,7 @@ existT is template universe polymorphic
 Argument A is implicit
 Argument scopes are [type_scope function_scope _ _]
 Expands to: Constructor Coq.Init.Specif.existT
-Inductive sigT (A : Type) (P : A -> Type) : Type :=
+Monomorphic Inductive sigT (A : Type) (P : A -> Type) : Type :=
     existT : forall x : A, P x -> {x : A & P x}
 
 For sigT: Argument A is implicit
@@ -14,7 +14,7 @@ For existT: Argument scopes are [type_scope function_scope _ _]
 existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
 
 Argument A is implicit
-Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 For eq: Argument A is implicit and maximally inserted
 For eq_refl, when applied to no arguments:
@@ -25,6 +25,7 @@ For eq: Argument scopes are [type_scope _ _]
 For eq_refl: Argument scopes are [type_scope _]
 eq_refl : forall (A : Type) (x : A), x = x
 
+eq_refl is not universe polymorphic
 When applied to no arguments:
   Arguments A, x are implicit and maximally inserted
 When applied to 1 argument:
@@ -37,7 +38,7 @@ When applied to no arguments:
   Arguments A, x are implicit and maximally inserted
 When applied to 1 argument:
   Argument A is implicit
-Nat.add = 
+Monomorphic Nat.add = 
 fix add (n m : nat) {struct n} : nat :=
   match n with
   | 0 => m
@@ -45,9 +46,11 @@ 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
 
+Nat.add is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 Nat.add is transparent
 Expands to: Constant Coq.Init.Nat.add
@@ -55,10 +58,11 @@ Nat.add : nat -> nat -> nat
 
 plus_n_O : forall n : nat, n = n + 0
 
+plus_n_O is not universe polymorphic
 Argument scope is [nat_scope]
 plus_n_O is opaque
 Expands to: Constant Coq.Init.Peano.plus_n_O
-Inductive le (n : nat) : nat -> Prop :=
+Monomorphic Inductive le (n : nat) : nat -> Prop :=
     le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
 
 For le_S: Argument m is implicit
@@ -68,18 +72,21 @@ For le_n: Argument scope is [nat_scope]
 For le_S: Argument scopes are [nat_scope nat_scope _]
 comparison : Set
 
+comparison is not universe polymorphic
 Expands to: Inductive Coq.Init.Datatypes.comparison
-Inductive comparison : Set :=
+Monomorphic Inductive comparison : Set :=
     Eq : comparison | Lt : comparison | Gt : comparison
 bar : foo
 
+bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
 Argument x is implicit and maximally inserted
 Expands to: Constant PrintInfos.bar
-*** [ bar : foo ]
+Monomorphic *** [ bar : foo ]
 
+bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
@@ -87,7 +94,7 @@ Argument x is implicit and maximally inserted
 Module Coq.Init.Peano
 Notation sym_eq := eq_sym
 Expands to: Notation Coq.Init.Logic.sym_eq
-Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 For eq: Argument A is implicit and maximally inserted
 For eq_refl, when applied to no arguments:
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
index f94ed64234..f080f6d0f0 100644
--- a/test-suite/output/TranspModtype.out
+++ b/test-suite/output/TranspModtype.out
@@ -1,7 +1,15 @@
-TrM.A = M.A
+Monomorphic TrM.A = M.A
      : Set
-OpM.A = M.A
+
+TrM.A is not universe polymorphic
+Monomorphic OpM.A = M.A
      : Set
-TrM.B = M.B
+
+OpM.A is not universe polymorphic
+Monomorphic TrM.B = M.B
      : Set
-*** [ OpM.B : Set ]
+
+TrM.B is not universe polymorphic
+Monomorphic *** [ OpM.B : Set ]
+
+OpM.B is not universe polymorphic
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index acc37f653c..49c292c501 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -1,34 +1,37 @@
-NonCumulative Inductive Empty@{u} : Type@{u} :=  
-NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A }
+Polymorphic NonCumulative Inductive Empty@{u} : Type@{u} :=  
+Polymorphic NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap
+  { punwrap : A }
 
 PWrap has primitive projections with eta conversion.
 For PWrap: Argument scope is [type_scope]
 For pwrap: Argument scopes are [type_scope _]
-punwrap@{u} = 
+Polymorphic punwrap@{u} = 
 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 _]
-NonCumulative Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A }
+Polymorphic NonCumulative Record RWrap (A : Type@{u}) : Type@{u} := rwrap
+  { runwrap : A }
 
 For RWrap: Argument scope is [type_scope]
 For rwrap: Argument scopes are [type_scope _]
-runwrap@{u} = 
+Polymorphic runwrap@{u} = 
 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
+Polymorphic Wrap@{u} = 
+fun A : Type@{u} => A
      : Type@{u} -> Type@{u}
 (* u |=  *)
 
 Wrap is universe polymorphic
 Argument scope is [type_scope]
-wrap@{u} = 
+Polymorphic wrap@{u} = 
 fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
      : forall A : Type@{u}, Wrap@{u} A -> A
 (* u |=  *)
@@ -36,13 +39,13 @@ fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
 wrap is universe polymorphic
 Arguments A, Wrap are implicit and maximally inserted
 Argument scopes are [type_scope _]
-bar@{u} = nat
+Polymorphic bar@{u} = nat
      : Wrap@{u} Set
 (* u |= Set < u
          *)
 
 bar is universe polymorphic
-foo@{u UnivBinders.17 v} = 
+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 |=  *)
@@ -75,25 +78,28 @@ mono
      : Type@{mono.u+1}
 The command has indeed failed with message:
 Universe u already exists.
-bobmorane = 
+Monomorphic bobmorane = 
 let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff
      : Type@{max(tt.u,ff.u)}
+
+bobmorane is not universe polymorphic
 The command has indeed failed with message:
 Universe u already bound.
-foo@{E M N} = 
+Polymorphic 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} = 
+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
-NonCumulative Inductive Empty@{E} : Type@{E} :=  
-NonCumulative Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
+Polymorphic NonCumulative Inductive Empty@{E} : Type@{E} :=  
+Polymorphic NonCumulative Record PWrap (A : Type@{E}) : Type@{E} := pwrap
+  { punwrap : A }
 
 PWrap has primitive projections with eta conversion.
 For PWrap: Argument scope is [type_scope]
@@ -119,45 +125,47 @@ Type@{bind_univs.mono.u}
 (* {bind_univs.mono.u} |=  *)
 
 bind_univs.mono is not universe polymorphic
-bind_univs.poly@{u} = Type@{u}
+Polymorphic bind_univs.poly@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
 
 bind_univs.poly is universe polymorphic
-insec@{v} = Type@{u} -> Type@{v}
+Polymorphic insec@{v} = 
+Type@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* v |=  *)
 
 insec is universe polymorphic
-NonCumulative Inductive insecind@{k} : Type@{k+1} :=
+Polymorphic NonCumulative 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}
+Polymorphic insec@{u v} = 
+Type@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
 
 insec is universe polymorphic
-NonCumulative Inductive insecind@{u k} : Type@{k+1} :=
+Polymorphic NonCumulative Inductive insecind@{u k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{u k}
 
 For inseccstr: Argument scope is [type_scope]
-inmod@{u} = Type@{u}
+Polymorphic inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
 
 inmod is universe polymorphic
-SomeMod.inmod@{u} = Type@{u}
+Polymorphic SomeMod.inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
 
 SomeMod.inmod is universe polymorphic
-inmod@{u} = Type@{u}
+Polymorphic inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
 
 inmod is universe polymorphic
-Applied.infunct@{u v} = 
+Polymorphic Applied.infunct@{u v} = 
 inmod@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out
index 773533a8d3..3dad2360c4 100644
--- a/test-suite/output/goal_output.out
+++ b/test-suite/output/goal_output.out
@@ -1,7 +1,11 @@
-Nat.t = nat
+Monomorphic Nat.t = nat
      : Set
-Nat.t = nat
+
+Nat.t is not universe polymorphic
+Monomorphic 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 f7ffd1959a..a1326596bb 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -1,9 +1,11 @@
-P = 
+Monomorphic P = 
 fun e : option L => match e with
                     | Some cl => Some cl
                     | 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