Fixes in the test-suite after modularisation of ZArith and co

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14114 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 8 insertions, 10 deletions

diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 93eff64c90..9bce8db4df 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -26,7 +26,6 @@ implb: bool -> bool -> bool
 comparison_beq: comparison -> comparison -> bool
 bool_beq: bool -> bool -> bool
 andb: bool -> bool -> bool
-Empty_set_beq: Empty_set -> Empty_set -> bool
 pred_Sn: forall n : nat, n = pred (S n)
 plus_n_Sm: forall n m : nat, S (n + m) = n + S m
 plus_n_O: forall n : nat, n = n + 0
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 0c32f8d8d9..4710de3dc1 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -22,7 +22,6 @@ implb: bool -> bool -> bool
 comparison_beq: comparison -> comparison -> bool
 bool_beq: bool -> bool -> bool
 andb: bool -> bool -> bool
-Empty_set_beq: Empty_set -> Empty_set -> bool
 S: nat -> nat
 O: nat
 pred: nat -> nat
diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out
index f23198b0f3..1b7a290352 100644
--- a/test-suite/output/ZSyntax.out
+++ b/test-suite/output/ZSyntax.out
@@ -16,11 +16,11 @@ fun x : positive => (- Zpos x~0)%Z
      : positive -> Z
 fun x : positive => (- Zpos x~0 + 0)%Z
      : positive -> Z
-(Z_of_nat 0 + 1)%Z
+(Z.of_nat 0 + 1)%Z
      : Z
-(0 + Z_of_nat (0 + 0))%Z
+(0 + Z.of_nat (0 + 0))%Z
      : Z
-Z_of_nat 0 = 0%Z
+Z.of_nat 0 = 0%Z
      : Prop
-(0 + Z_of_nat 11)%Z
+(0 + Z.of_nat 11)%Z
      : Z
diff --git a/test-suite/output/ZSyntax.v b/test-suite/output/ZSyntax.v
index 289a1e3f49..d3640cae44 100644
--- a/test-suite/output/ZSyntax.v
+++ b/test-suite/output/ZSyntax.v
@@ -8,10 +8,10 @@ Check (fun x : positive => Zneg (xO x)).
 Check (fun x : positive => (Zpos (xO x) + 0)%Z).
 Check (fun x : positive => (- Zpos (xO x))%Z).
 Check (fun x : positive => (- Zpos (xO x) + 0)%Z).
-Check (Z_of_nat 0 + 1)%Z.
-Check (0 + Z_of_nat (0 + 0))%Z.
-Check (Z_of_nat 0 = 0%Z).
+Check (Z.of_nat 0 + 1)%Z.
+Check (0 + Z.of_nat (0 + 0))%Z.
+Check (Z.of_nat 0 = 0%Z).
 
 (* Submitted by Pierre Casteran *)
 Require Import Arith.
-Check (0 + Z_of_nat 11)%Z.
+Check (0 + Z.of_nat 11)%Z.