Upgrading output tests.

output/Arguments.v
output/ArgumentsScope.v
output/Arguments_renaming.v
output/Cases.v
output/Implicit.v
output/PrintInfos.v
output/TranspModType.v

Main changes: monomorphic -> not universe polymorphic, Peano vs Nat

9 files changed, 95 insertions, 95 deletions

diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index e0e8211d5..dc421830f 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -1,48 +1,48 @@
-minus : nat -> nat -> nat
+Nat.sub : nat -> nat -> nat
 
-minus is monomorphic
+Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
-The reduction tactics unfold minus avoiding to expose match constructs
-minus is transparent
-Expands to: Constant Coq.Init.Peano.minus
-minus : nat -> nat -> nat
+The reduction tactics unfold Nat.sub avoiding to expose match constructs
+Nat.sub is transparent
+Expands to: Constant Coq.Init.Nat.sub
+Nat.sub : nat -> nat -> nat
 
-minus is monomorphic
+Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
-The reduction tactics unfold minus when applied to 1 argument
+The reduction tactics unfold Nat.sub when applied to 1 argument
   avoiding to expose match constructs
-minus is transparent
-Expands to: Constant Coq.Init.Peano.minus
-minus : nat -> nat -> nat
+Nat.sub is transparent
+Expands to: Constant Coq.Init.Nat.sub
+Nat.sub : nat -> nat -> nat
 
-minus is monomorphic
+Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
-The reduction tactics unfold minus
+The reduction tactics unfold Nat.sub
   when the 1st argument evaluates to a constructor and
   when applied to 1 argument avoiding to expose match constructs
-minus is transparent
-Expands to: Constant Coq.Init.Peano.minus
-minus : nat -> nat -> nat
+Nat.sub is transparent
+Expands to: Constant Coq.Init.Nat.sub
+Nat.sub : nat -> nat -> nat
 
-minus is monomorphic
+Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
-The reduction tactics unfold minus when the 1st and
+The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor and when applied to 2 arguments 
-minus is transparent
-Expands to: Constant Coq.Init.Peano.minus
-minus : nat -> nat -> nat
+Nat.sub is transparent
+Expands to: Constant Coq.Init.Nat.sub
+Nat.sub : nat -> nat -> nat
 
-minus is monomorphic
+Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
-The reduction tactics unfold minus when the 1st and
+The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor 
-minus is transparent
-Expands to: Constant Coq.Init.Peano.minus
+Nat.sub is transparent
+Expands to: Constant Coq.Init.Nat.sub
 pf :
 forall D1 C1 : Type,
 (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
 
-pf is monomorphic
+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 _ _ _ _ _]
@@ -51,7 +51,7 @@ pf is transparent
 Expands to: Constant Top.pf
 fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
 
-fcomp is monomorphic
+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 
@@ -59,20 +59,20 @@ fcomp is transparent
 Expands to: Constant Top.fcomp
 volatile : nat -> nat
 
-volatile is monomorphic
+volatile is not universe polymorphic
 Argument scope is [nat_scope]
 The reduction tactics always unfold volatile
 volatile is transparent
 Expands to: Constant Top.volatile
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
-f is monomorphic
+f is not universe polymorphic
 Argument scopes are [_ _ nat_scope _ nat_scope]
 f is transparent
 Expands to: Constant Top.S1.S2.f
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
-f is monomorphic
+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 
@@ -80,7 +80,7 @@ f is transparent
 Expands to: Constant Top.S1.S2.f
 f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
-f is monomorphic
+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
@@ -89,7 +89,7 @@ f is transparent
 Expands to: Constant Top.S1.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
-f is monomorphic
+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
@@ -102,7 +102,7 @@ Expands to: Constant Top.f
      : Prop
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
-f is monomorphic
+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/Arguments.v b/test-suite/output/Arguments.v
index 4d4ab54f1..05eeaac63 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -1,13 +1,13 @@
-Arguments minus n m : simpl nomatch. 
-About minus.
-Arguments minus n / m : simpl nomatch. 
-About minus.
-Arguments minus !n / m : simpl nomatch. 
-About minus.
-Arguments minus !n !m /.
-About minus.
-Arguments minus !n !m.
-About minus.
+Arguments Nat.sub n m : simpl nomatch.
+About Nat.sub.
+Arguments Nat.sub n / m : simpl nomatch.
+About Nat.sub.
+Arguments Nat.sub !n / m : simpl nomatch.
+About Nat.sub.
+Arguments Nat.sub !n !m /.
+About Nat.sub.
+Arguments Nat.sub !n !m.
+About Nat.sub.
 Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := 
   fun x => (f (fst x), g (snd x)).
 Delimit Scope foo_scope with F.
@@ -44,7 +44,7 @@ Record r := { pi :> nat -> bool -> unit }.
 Notation "$" := 3 (only parsing) : foo_scope.
 Notation "$" := true (only parsing) : bar_scope.
 Delimit Scope bar_scope with B.
-Arguments pi _ _%F _%B. 
+Arguments pi _ _%F _%B.
 Check (forall w : r, pi w $ $ = tt).
 Fail Check (forall w : r, w $ $ = tt).
 Axiom w : r.
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index 358a96bc3..71d5fc78b 100644
--- a/test-suite/output/ArgumentsScope.out
+++ b/test-suite/output/ArgumentsScope.out
@@ -1,70 +1,70 @@
 a : bool -> bool
 
-a is monomorphic
+a is not universe polymorphic
 Argument scope is [bool_scope]
 Expands to: Variable a
 b : bool -> bool
 
-b is monomorphic
+b is not universe polymorphic
 Argument scope is [bool_scope]
 Expands to: Variable b
 negb'' : bool -> bool
 
-negb'' is monomorphic
+negb'' is not universe polymorphic
 Argument scope is [bool_scope]
 negb'' is transparent
 Expands to: Constant Top.A.B.negb''
 negb' : bool -> bool
 
-negb' is monomorphic
+negb' is not universe polymorphic
 Argument scope is [bool_scope]
 negb' is transparent
 Expands to: Constant Top.A.negb'
 negb : bool -> bool
 
-negb is monomorphic
+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 monomorphic
+a is not universe polymorphic
 Expands to: Variable a
 b : bool -> bool
 
-b is monomorphic
+b is not universe polymorphic
 Expands to: Variable b
 negb : bool -> bool
 
-negb is monomorphic
+negb is not universe polymorphic
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
 negb' : bool -> bool
 
-negb' is monomorphic
+negb' is not universe polymorphic
 negb' is transparent
 Expands to: Constant Top.A.negb'
 negb'' : bool -> bool
 
-negb'' is monomorphic
+negb'' is not universe polymorphic
 negb'' is transparent
 Expands to: Constant Top.A.B.negb''
 a : bool -> bool
 
-a is monomorphic
+a is not universe polymorphic
 Expands to: Variable a
 negb : bool -> bool
 
-negb is monomorphic
+negb is not universe polymorphic
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
 negb' : bool -> bool
 
-negb' is monomorphic
+negb' is not universe polymorphic
 negb' is transparent
 Expands to: Constant Top.negb'
 negb'' : bool -> bool
 
-negb'' is monomorphic
+negb'' is not universe polymorphic
 negb'' is transparent
 Expands to: Constant Top.negb''
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index c440d5ba7..c99dfc018 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -20,7 +20,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 monomorphic
+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
@@ -36,7 +36,7 @@ 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 monomorphic
+myrefl is not universe polymorphic
 Arguments are renamed to C, x, _
 Argument C is implicit and maximally inserted
 Argument scopes are [type_scope _ _]
@@ -49,13 +49,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
-myplus is monomorphic
+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 monomorphic
+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]
@@ -74,7 +74,7 @@ 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 monomorphic
+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 _ _]
@@ -89,13 +89,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
-myplus is monomorphic
+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 monomorphic
+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/Cases.out b/test-suite/output/Cases.out
index 152a722aa..c768f09ce 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -7,7 +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 monomorphic
+t_rect is not universe polymorphic
 proj = 
 fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) =>
 match Nat.eq_dec x y with
@@ -18,7 +18,7 @@ match Nat.eq_dec x y with
 end
      : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
 
-proj is monomorphic
+proj is not universe polymorphic
 Argument scopes are [nat_scope nat_scope _ _ _]
 foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
@@ -29,7 +29,7 @@ fix foo (A : Type) (l : list A) {struct l} : option A :=
   end
      : forall A : Type, list A -> option A
 
-foo is monomorphic
+foo is not universe polymorphic
 Argument scopes are [type_scope list_scope]
 uncast = 
 fun (A : Type) (x : I A) => match x with
@@ -37,12 +37,12 @@ fun (A : Type) (x : I A) => match x with
                             end
      : forall A : Type, I A -> A
 
-uncast is monomorphic
+uncast is not universe polymorphic
 Argument scopes are [type_scope _]
 foo' = if A 0 then true else false
      : bool
 
-foo' is monomorphic
+foo' is not universe polymorphic
 f = 
 fun H : B =>
 match H with
@@ -54,4 +54,4 @@ match H with
 end
      : B -> True
 
-f is monomorphic
+f is not universe polymorphic
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index d1cd5e84f..0b0f501f9 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -5,7 +5,7 @@ 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 monomorphic
+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/PrintInfos.out b/test-suite/output/PrintInfos.out
index 62889f802..2b010f067 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -25,7 +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 monomorphic
+eq_refl is not universe polymorphic
 When applied to no arguments:
   Arguments A, x are implicit and maximally inserted
 When applied to 1 argument:
@@ -38,27 +38,27 @@ When applied to no arguments:
   Arguments A, x are implicit and maximally inserted
 When applied to 1 argument:
   Argument A is implicit
-plus = 
-fix plus (n m : nat) {struct n} : nat :=
+Nat.add = 
+fix add (n m : nat) {struct n} : nat :=
   match n with
   | 0 => m
-  | S p => S (plus p m)
+  | S p => S (add p m)
   end
      : nat -> nat -> nat
 
-plus is monomorphic
+Nat.add is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
-plus : nat -> nat -> nat
+Nat.add : nat -> nat -> nat
 
-plus is monomorphic
+Nat.add is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
-plus is transparent
-Expands to: Constant Coq.Init.Peano.plus
-plus : nat -> nat -> nat
+Nat.add is transparent
+Expands to: Constant Coq.Init.Nat.add
+Nat.add : nat -> nat -> nat
 
 plus_n_O : forall n : nat, n = n + 0
 
-plus_n_O is monomorphic
+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
@@ -80,13 +80,13 @@ For le_n: Argument scope is [nat_scope]
 For le_S: Argument scopes are [nat_scope nat_scope _]
 comparison : Set
 
-comparison is monomorphic
+comparison is not universe polymorphic
 Expands to: Inductive Coq.Init.Datatypes.comparison
 Inductive comparison : Set :=
     Eq : comparison | Lt : comparison | Gt : comparison
 bar : foo
 
-bar is monomorphic
+bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
@@ -94,14 +94,14 @@ Argument x is implicit and maximally inserted
 Expands to: Constant Top.bar
 *** [ bar : foo ]
 
-bar is monomorphic
+bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
 Argument x is implicit and maximally inserted
 bar : foo
 
-bar is monomorphic
+bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
@@ -109,7 +109,7 @@ Argument x is implicit and maximally inserted
 Expands to: Constant Top.bar
 *** [ bar : foo ]
 
-bar is monomorphic
+bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
index deeb1f656..4edeeb232 100644
--- a/test-suite/output/PrintInfos.v
+++ b/test-suite/output/PrintInfos.v
@@ -6,9 +6,9 @@ Print eq_refl.
 About eq_refl.
 Print Implicit eq_refl.
 
-Print plus.
-About plus.
-Print Implicit plus.
+Print Nat.add.
+About Nat.add.
+Print Implicit Nat.add.
 
 About plus_n_O.
 
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
index dbbd73dcd..67b65d4b8 100644
--- a/test-suite/output/TranspModtype.out
+++ b/test-suite/output/TranspModtype.out
@@ -1,15 +1,15 @@
 TrM.A = M.A
      : Set
 
-TrM.A is monomorphic
+TrM.A is not universe polymorphic
 OpM.A = M.A
      : Set
 
-OpM.A is monomorphic
+OpM.A is not universe polymorphic
 TrM.B = M.B
      : Set
 
-TrM.B is monomorphic
+TrM.B is not universe polymorphic
 *** [ OpM.B : Set ]
 
-OpM.B is monomorphic
+OpM.B is not universe polymorphic