aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--printing/prettyp.ml2
-rw-r--r--printing/printer.ml8
-rw-r--r--printing/printer.mli2
-rw-r--r--printing/printmod.ml10
-rw-r--r--test-suite/output/Arguments_renaming.out11
-rw-r--r--test-suite/output/Binder.out4
-rw-r--r--test-suite/output/Cases.out18
-rw-r--r--test-suite/output/Implicit.out3
-rw-r--r--test-suite/output/Inductive.out3
-rw-r--r--test-suite/output/InitSyntax.out2
-rw-r--r--test-suite/output/Load.out4
-rw-r--r--test-suite/output/Notations3.out6
-rw-r--r--test-suite/output/PatternsInBinders.out16
-rw-r--r--test-suite/output/PrintInfos.out14
-rw-r--r--test-suite/output/StringSyntax.out6
-rw-r--r--test-suite/output/TranspModtype.out8
-rw-r--r--test-suite/output/UnivBinders.out59
-rw-r--r--test-suite/output/goal_output.out4
-rw-r--r--test-suite/output/inference.out2
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:42:51 +0000