Stop printing Monomorphic/Polymorphic in Print.

You can tell which it is from the `@{}` if you really care, and seeing
`Monomorphic List (A:Type)` with no indication that `Monomorphic` is
about universes can confuse people.

19 files changed, 76 insertions, 106 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 8f7e4470f9..c417ef8a66 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -575,7 +575,7 @@ let print_constant with_values sep sp udecl =
   in
   let env = Global.env () and sigma = Evd.from_ctx ctx in
   let pr_ltype = pr_ltype_env env sigma in
-  hov 0 (pr_polymorphic (Declareops.constant_is_polymorphic cb) ++
+  hov 0 (
     match val_0 with
     | None ->
 	str"*** [ " ++
diff --git a/printing/printer.ml b/printing/printer.ml
index be0139da06..3f7837fd6e 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -982,14 +982,6 @@ let pr_assumptionset env sigma s =
     ] in
     prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
 
-let pr_cumulative poly cum =
-  if poly then
-    if cum then str "Cumulative " else str "NonCumulative "
-  else mt ()
-
-let pr_polymorphic b = 
-  if b then str"Polymorphic " else str"Monomorphic "
-
 (* 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 fd4682a086..9a06d555e4 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -81,8 +81,6 @@ val pr_sort                : evar_map -> Sorts.t -> Pp.t
 
 (** Universe constraints *)
 
-val pr_polymorphic         : bool -> Pp.t
-val pr_cumulative          : bool -> bool -> Pp.t
 val pr_universe_instance   : evar_map -> Univ.Instance.t -> Pp.t
 val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Constraint.t -> Pp.t
 val pr_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
diff --git a/printing/printmod.ml b/printing/printmod.ml
index a8d7b0c1a8..898f231a8b 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -123,11 +123,7 @@ let print_mutual_inductive env mind mib udecl =
       (Declareops.inductive_polymorphic_context mib) udecl
   in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
-  hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
-         Printer.pr_cumulative
-           (Declareops.inductive_is_polymorphic mib) 
-           (Declareops.inductive_is_cumulative mib) ++
-         def keyword ++ spc () ++
+  hov 0 (def keyword ++ spc () ++
          prlist_with_sep (fun () -> fnl () ++ str"  with ")
            (print_one_inductive env sigma mib) inds ++
          match mib.mind_universes with
@@ -172,10 +168,6 @@ let print_record env mind mib udecl =
   in
   hov 0 (
     hov 0 (
-      Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
-      Printer.pr_cumulative
-        (Declareops.inductive_is_polymorphic mib)
-        (Declareops.inductive_is_cumulative mib) ++
       def keyword ++ spc () ++ Id.print mip.mind_typename ++ brk(1,4) ++
       print_params env sigma params ++
       str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index b071da86c9..583ea0cb43 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]
-Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+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
@@ -31,8 +31,7 @@ When applied to 1 argument:
   Argument B is implicit
 Argument scopes are [type_scope _]
 Expands to: Constructor Coq.Init.Logic.eq_refl
-Monomorphic Inductive myEq (B : Type) (x : A) : A -> Prop :=
-    myrefl : B -> myEq B x x
+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
@@ -45,7 +44,7 @@ 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
-Monomorphic myplus = 
+myplus = 
 fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   match n with
   | 0 => m
@@ -69,7 +68,7 @@ myplus is transparent
 Expands to: Constant Arguments_renaming.Test1.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
-Monomorphic Inductive myEq (A B : Type) (x : A) : A -> Prop :=
+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, _
@@ -85,7 +84,7 @@ 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
-Monomorphic myplus = 
+myplus = 
 fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   match n with
   | 0 => m
diff --git a/test-suite/output/Binder.out b/test-suite/output/Binder.out
index 9c46ace463..6e27837b26 100644
--- a/test-suite/output/Binder.out
+++ b/test-suite/output/Binder.out
@@ -1,10 +1,10 @@
-Monomorphic foo = fun '(x, y) => x + y
+foo = fun '(x, y) => x + y
      : nat * nat -> nat
 
 foo is not universe polymorphic
 forall '(a, b), a /\ b
      : Prop
-Monomorphic foo = λ '(x, y), x + y
+foo = λ '(x, y), x + y
      : nat * nat → nat
 
 foo is not universe polymorphic
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 0a02c5a7dd..efcc299e82 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -1,4 +1,4 @@
-Monomorphic t_rect = 
+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
@@ -17,7 +17,7 @@ Argument scopes are [function_scope function_scope _]
                      | {| f3 := b |} => b
                      end
      : TT -> 0 = 0
-Monomorphic proj = 
+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
@@ -29,7 +29,7 @@ end
 
 proj is not universe polymorphic
 Argument scopes are [nat_scope nat_scope function_scope _ _]
-Monomorphic foo = 
+foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
   match l with
   | nil => None
@@ -40,7 +40,7 @@ fix foo (A : Type) (l : list A) {struct l} : option A :=
 
 foo is not universe polymorphic
 Argument scopes are [type_scope list_scope]
-Monomorphic uncast = 
+uncast = 
 fun (A : Type) (x : I A) => match x with
                             | x0 <: _ => x0
                             end
@@ -48,11 +48,11 @@ fun (A : Type) (x : I A) => match x with
 
 uncast is not universe polymorphic
 Argument scopes are [type_scope _]
-Monomorphic foo' = if A 0 then true else false
+foo' = if A 0 then true else false
      : bool
 
 foo' is not universe polymorphic
-Monomorphic f = 
+f = 
 fun H : B =>
 match H with
 | AC x =>
@@ -83,18 +83,18 @@ 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.
-Monomorphic lem1 = 
+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
-Monomorphic lem2 = 
+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]
-Monomorphic lem3 = 
+lem3 = 
 fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
      : forall k : nat * nat, k = k
 
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 71c7070f2b..0b0f501f9a 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -2,8 +2,7 @@ compose (C:=nat) S
      : (nat -> nat) -> nat -> nat
 ex_intro (P:=fun _ : nat => True) (x:=0) I
      : ex (fun _ : nat => True)
-Monomorphic d2 = 
-fun x : nat => d1 (y:=x)
+d2 = fun x : nat => d1 (y:=x)
      : forall x x0 : nat, x0 = x -> x0 = x
 
 d2 is not universe polymorphic
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index 5a548cfae4..2ba02924c9 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -1,8 +1,7 @@
 The command has indeed failed with message:
 Last occurrence of "list'" must have "A" as 1st argument in
  "A -> list' A -> list' (A * A)".
-Monomorphic Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=
-    Foo : foo A x
+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 4743fb0d0a..c17c63e724 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -1,4 +1,4 @@
-Monomorphic Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
+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 f84cedfa62..ebbd5d422b 100644
--- a/test-suite/output/Load.out
+++ b/test-suite/output/Load.out
@@ -1,8 +1,8 @@
-Monomorphic f = 2
+f = 2
      : nat
 
 f is not universe polymorphic
-Monomorphic u = I
+u = I
      : True
 
 u is not universe polymorphic
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index f53313def9..71d92482d0 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -225,7 +225,7 @@ fun S : nat => [[S | S + S]]
      : Set
 exists2 '{{y, z}} : nat * nat, y > z & z > y
      : Prop
-Monomorphic foo = 
+foo = 
 fun l : list nat => match l with
                     | _ :: (_ :: _) as l1 => l1
                     | _ => l
@@ -261,11 +261,11 @@ myfoo01 tt
  {4; 5; 6};
  {7; 8; 9}]
      : list (list nat)
-Monomorphic amatch = mmatch 0 (with 0 => 1| 1 => 2 end)
+amatch = mmatch 0 (with 0 => 1| 1 => 2 end)
      : unit
 
 amatch is not universe polymorphic
-Monomorphic alist = [0; 1; 2]
+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 bfeff20524..bdbc5a5960 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -1,4 +1,4 @@
-Monomorphic swap = fun '(x, y) => (y, x)
+swap = fun '(x, y) => (y, x)
      : A * B -> B * A
 
 swap is not universe polymorphic
@@ -6,22 +6,20 @@ fun '(x, y) => (y, x)
      : A * B -> B * A
 forall '(x, y), swap (x, y) = (y, x)
      : Prop
-Monomorphic proj_informative = 
-fun '(exist _ x _) => x : A
+proj_informative = fun '(exist _ x _) => x : A
      : {x : A | P x} -> A
 
 proj_informative is not universe polymorphic
-Monomorphic foo = 
-fun '(Bar n b tt p) => if b then n + p else n - p
+foo = fun '(Bar n b tt p) => if b then n + p else n - p
      : Foo -> nat
 
 foo is not universe polymorphic
-Monomorphic baz = 
+baz = 
 fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1
      : Foo -> Foo -> nat
 
 baz is not universe polymorphic
-Monomorphic swap = 
+swap = 
 fun (A B : Type) '(x, y) => (y, x)
      : forall A B : Type, A * B -> B * A
 
@@ -40,7 +38,7 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w)
      : A * B → B * A
 ∀ '(x, y), swap (x, y) = (y, x)
      : Prop
-Monomorphic both_z = 
+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
@@ -52,7 +50,7 @@ forall '(x, y) '(z, t), swap (x, y) = (z, t)
      : Prop
 fun (pat : nat) '(x, y) => x + y = pat
      : nat -> nat * nat -> Prop
-Monomorphic f = fun x : nat => x + x
+f = fun x : nat => x + x
      : nat -> nat
 
 f is not universe polymorphic
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index be793dd453..da1fca7134 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
-Monomorphic Inductive sigT (A : Type) (P : A -> Type) : Type :=
+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
-Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+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:
@@ -38,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
-Monomorphic Nat.add = 
+Nat.add = 
 fix add (n m : nat) {struct n} : nat :=
   match n with
   | 0 => m
@@ -62,7 +62,7 @@ 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
-Monomorphic Inductive le (n : nat) : nat -> Prop :=
+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
@@ -74,7 +74,7 @@ comparison : Set
 
 comparison is not universe polymorphic
 Expands to: Inductive Coq.Init.Datatypes.comparison
-Monomorphic Inductive comparison : Set :=
+Inductive comparison : Set :=
     Eq : comparison | Lt : comparison | Gt : comparison
 bar : foo
 
@@ -84,7 +84,7 @@ bar : forall x : nat, x = 0
 
 Argument x is implicit and maximally inserted
 Expands to: Constant PrintInfos.bar
-Monomorphic *** [ bar : foo ]
+*** [ bar : foo ]
 
 bar is not universe polymorphic
 Expanded type for implicit arguments
@@ -94,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
-Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+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/StringSyntax.out b/test-suite/output/StringSyntax.out
index bbc936766d..c7e6ef950e 100644
--- a/test-suite/output/StringSyntax.out
+++ b/test-suite/output/StringSyntax.out
@@ -1,4 +1,4 @@
-Monomorphic byte_rect = 
+byte_rect = 
 fun (P : byte -> Type) (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 "?") 
   (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") 
   (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") 
@@ -435,7 +435,7 @@ end
 
 byte_rect is not universe polymorphic
 Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope]
-Monomorphic byte_rec = 
+byte_rec = 
 fun P : byte -> Set => byte_rect P
      : forall P : byte -> Set,
        P "000" ->
@@ -610,7 +610,7 @@ fun P : byte -> Set => byte_rect P
 
 byte_rec is not universe polymorphic
 Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope]
-Monomorphic byte_ind = 
+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 "?") 
   (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") 
   (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") 
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
index f080f6d0f0..67b65d4b81 100644
--- a/test-suite/output/TranspModtype.out
+++ b/test-suite/output/TranspModtype.out
@@ -1,15 +1,15 @@
-Monomorphic TrM.A = M.A
+TrM.A = M.A
      : Set
 
 TrM.A is not universe polymorphic
-Monomorphic OpM.A = M.A
+OpM.A = M.A
      : Set
 
 OpM.A is not universe polymorphic
-Monomorphic TrM.B = M.B
+TrM.B = M.B
      : Set
 
 TrM.B is not universe polymorphic
-Monomorphic *** [ OpM.B : Set ]
+*** [ OpM.B : Set ]
 
 OpM.B is not universe polymorphic
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 4d3f7419e6..0bd6ade690 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -1,37 +1,34 @@
-Polymorphic NonCumulative Inductive Empty@{u} : Type@{u} :=  
-Polymorphic NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap
-  { punwrap : A }
+Inductive Empty@{u} : Type@{u} :=  
+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 _]
-Polymorphic punwrap@{u} = 
+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 _]
-Polymorphic NonCumulative Record RWrap (A : Type@{u}) : Type@{u} := rwrap
-  { runwrap : A }
+Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A }
 
 For RWrap: Argument scope is [type_scope]
 For rwrap: Argument scopes are [type_scope _]
-Polymorphic runwrap@{u} = 
+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 _]
-Polymorphic Wrap@{u} = 
-fun A : Type@{u} => A
+Wrap@{u} = fun A : Type@{u} => A
      : Type@{u} -> Type@{u}
 (* u |=  *)
 
 Wrap is universe polymorphic
 Argument scope is [type_scope]
-Polymorphic wrap@{u} = 
+wrap@{u} = 
 fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
      : forall A : Type@{u}, Wrap@{u} A -> A
 (* u |=  *)
@@ -39,12 +36,12 @@ 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 _]
-Polymorphic bar@{u} = nat
+bar@{u} = nat
      : Wrap@{u} Set
 (* u |= Set < u *)
 
 bar is universe polymorphic
-Polymorphic foo@{u UnivBinders.17 v} = 
+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 |=  *)
@@ -56,7 +53,7 @@ Type@{i} -> Type@{j}
      = Type@{i} -> Type@{j}
      : Type@{max(i+1,j+1)}
 (* {j i} |=  *)
-Monomorphic mono = Type@{mono.u}
+mono = Type@{mono.u}
      : Type@{mono.u+1}
 (* {mono.u} |=  *)
 
@@ -77,7 +74,7 @@ mono
      : Type@{mono.u+1}
 The command has indeed failed with message:
 Universe u already exists.
-Monomorphic bobmorane = 
+bobmorane = 
 let tt := Type@{UnivBinders.32} in
 let ff := Type@{UnivBinders.34} in tt -> ff
      : Type@{max(UnivBinders.31,UnivBinders.33)}
@@ -85,21 +82,20 @@ let ff := Type@{UnivBinders.34} in tt -> ff
 bobmorane is not universe polymorphic
 The command has indeed failed with message:
 Universe u already bound.
-Polymorphic foo@{E M N} = 
+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
-Polymorphic foo@{u UnivBinders.17 v} = 
+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
-Polymorphic NonCumulative Inductive Empty@{E} : Type@{E} :=  
-Polymorphic NonCumulative Record PWrap (A : Type@{E}) : Type@{E} := pwrap
-  { punwrap : A }
+Inductive Empty@{E} : Type@{E} :=  
+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,58 +115,55 @@ The command has indeed failed with message:
 This object does not support universe names.
 The command has indeed failed with message:
 Cannot enforce v < u because u < gU < gV < v
-Monomorphic bind_univs.mono = 
+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
-Polymorphic bind_univs.poly@{u} = Type@{u}
+bind_univs.poly@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
 
 bind_univs.poly is universe polymorphic
-Polymorphic insec@{v} = 
-Type@{u} -> Type@{v}
+insec@{v} = Type@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* v |=  *)
 
 insec is universe polymorphic
-Polymorphic NonCumulative Inductive insecind@{k} : Type@{k+1} :=
-    inseccstr : Type@{k} -> insecind@{k}
+Inductive insecind@{k} : Type@{k+1} :=  inseccstr : Type@{k} -> insecind@{k}
 
 For inseccstr: Argument scope is [type_scope]
-Polymorphic insec@{u v} = 
-Type@{u} -> Type@{v}
+insec@{u v} = Type@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
 
 insec is universe polymorphic
-Polymorphic NonCumulative Inductive insecind@{u k} : Type@{k+1} :=
+Inductive insecind@{u k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{u k}
 
 For inseccstr: Argument scope is [type_scope]
-Polymorphic insec2@{u} = Prop
+insec2@{u} = Prop
      : Type@{Set+1}
 (* u |=  *)
 
 insec2 is universe polymorphic
-Polymorphic inmod@{u} = Type@{u}
+inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
 
 inmod is universe polymorphic
-Polymorphic SomeMod.inmod@{u} = Type@{u}
+SomeMod.inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
 
 SomeMod.inmod is universe polymorphic
-Polymorphic inmod@{u} = Type@{u}
+inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
 
 inmod is universe polymorphic
-Polymorphic Applied.infunct@{u v} = 
+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 3dad2360c4..20568f742a 100644
--- a/test-suite/output/goal_output.out
+++ b/test-suite/output/goal_output.out
@@ -1,8 +1,8 @@
-Monomorphic Nat.t = nat
+Nat.t = nat
      : Set
 
 Nat.t is not universe polymorphic
-Monomorphic Nat.t = nat
+Nat.t = nat
      : Set
 
 Nat.t is not universe polymorphic
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index a1326596bb..f545ca679c 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -1,4 +1,4 @@
-Monomorphic P = 
+P = 
 fun e : option L => match e with
                     | Some cl => Some cl
                     | None => None