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

6 files changed, 12 insertions, 15 deletions

diff --git a/test-suite/complexity/ring2.v b/test-suite/complexity/ring2.v
index ab57afdbb..6945edc88 100644
--- a/test-suite/complexity/ring2.v
+++ b/test-suite/complexity/ring2.v
@@ -11,7 +11,7 @@ match x with
     | 0%Z => x
     | Zpos y' => Zpos (x' + y')
     | Zneg y' =>
-        match (x' ?= y')%positive Eq with
+        match (x' ?= y')%positive with
         | Eq => 0%Z
         | Lt => Zneg (y' - x')
         | Gt => Zpos (x' - y')
@@ -21,7 +21,7 @@ match x with
     match y with
     | 0%Z => x
     | Zpos y' =>
-        match (x' ?= y')%positive Eq with
+        match (x' ?= y')%positive with
         | Eq => 0%Z
         | Lt => Zpos (y' - x')
         | Gt => Zneg (x' - y')
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 93eff64c9..9bce8db4d 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 0c32f8d8d..4710de3dc 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 f23198b0f..1b7a29035 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 289a1e3f4..d3640cae4 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.
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
index be4e06845..b25b502cf 100644
--- a/test-suite/success/fix.v
+++ b/test-suite/success/fix.v
@@ -9,13 +9,12 @@ Inductive rBoolOp : Set :=
   | rAnd : rBoolOp
   | rEq : rBoolOp.
 
-Definition rlt (a b : rNat) : Prop :=
-  (a ?= b)%positive Datatypes.Eq = Datatypes.Lt.
+Definition rlt (a b : rNat) : Prop := Pcompare a b Eq = Lt.
 
 Definition rltDec : forall m n : rNat, {rlt m n} + {rlt n m \/ m = n}.
 intros n m; generalize (nat_of_P_lt_Lt_compare_morphism n m);
  generalize (nat_of_P_gt_Gt_compare_morphism n m);
- generalize (Pcompare_Eq_eq n m); case ((n ?= m)%positive Datatypes.Eq).
+ generalize (Pcompare_Eq_eq n m); case (Pcompare n m Eq).
 intros H' H'0 H'1; right; right; auto.
 intros H' H'0 H'1; left; unfold rlt in |- *.
 apply nat_of_P_lt_Lt_compare_complement_morphism; auto.