Minor fixes in the test-suite after my recent commits

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

6 files changed, 13 insertions, 15 deletions

diff --git a/test-suite/complexity/ring2.v b/test-suite/complexity/ring2.v
index c3634f640..52dae265b 100644
--- a/test-suite/complexity/ring2.v
+++ b/test-suite/complexity/ring2.v
@@ -3,7 +3,7 @@
 
 Require Import BinInt Zbool.
 
-Definition Z.add x y :=
+Definition Zadd x y :=
 match x with
 | 0%Z => y
 | Zpos x' =>
@@ -30,9 +30,10 @@ match x with
     end
 end.
 
+
 Require Import Ring.
 
-Lemma Zth : ring_theory Z0 (Zpos xH) Z.add Z.mul Z.sub Z.opp (@eq Z).
+Lemma Zth : ring_theory Z0 (Zpos xH) Zadd Z.mul Z.sub Z.opp (@eq Z).
 Admitted.
 
 Ltac Zcst t :=
@@ -45,7 +46,7 @@ Add Ring Zr : Zth
   (decidable Zeq_bool_eq, constants [Zcst]).
 
 Open Scope Z_scope.
-Infix "+" := Z.add : Z_scope.
+Infix "+" := Zadd : Z_scope.
 
 Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13.
 Timeout 5 Time intro; ring.
diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v
index 4a1231b35..25e4a09fa 100644
--- a/test-suite/micromega/example.v
+++ b/test-suite/micromega/example.v
@@ -8,7 +8,6 @@
 
 Require Import ZArith.
 Require Import Psatz.
-Require Import Ring_normalize.
 Open Scope Z_scope.
 Require Import ZMicromega.
 Require Import VarMap.
diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v
index 76dc52e6c..47e6005b9 100644
--- a/test-suite/micromega/qexample.v
+++ b/test-suite/micromega/qexample.v
@@ -8,7 +8,6 @@
 
 Require Import Psatz.
 Require Import QArith.
-Require Import Ring_normalize.
 
 Lemma plus_minus : forall x y,
   0 == x + y -> 0 ==  x -y -> 0 == x /\ 0 == y.
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index 9bb9daccb..2eed7e951 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -8,7 +8,6 @@
 
 Require Import Psatz.
 Require Import Reals.
-Require Import Ring_normalize.
 
 Open Scope R_scope.
 
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index 6fa547358..8767f6874 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -9,11 +9,11 @@
 Require Import ZArith Zwf Psatz QArith.
 Open Scope Z_scope.
 
-Lemma Z.abs_square : forall x,  (Z.abs  x)^2 = x^2.
+Lemma Zabs_square : forall x,  (Z.abs  x)^2 = x^2.
 Proof.
  intros ; case (Zabs_dec x) ; intros ; psatz Z 2.
 Qed.
-Hint Resolve Z.abs_nonneg Z.abs_square.
+Hint Resolve Z.abs_nonneg Zabs_square.
 
 Lemma integer_statement :  ~exists n, exists p, n^2 = 2*p^2 /\ n <> 0.
 Proof.
diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out
index 1b7a29035..dc41b0aa4 100644
--- a/test-suite/output/ZSyntax.out
+++ b/test-suite/output/ZSyntax.out
@@ -2,19 +2,19 @@
      : Z
 fun f : nat -> Z => (f 0%nat + 0)%Z
      : (nat -> Z) -> Z
-fun x : positive => Zpos x~0
+fun x : positive => Z.pos x~0
      : positive -> Z
-fun x : positive => (Zpos x + 1)%Z
+fun x : positive => (Z.pos x + 1)%Z
      : positive -> Z
-fun x : positive => Zpos x
+fun x : positive => Z.pos x
      : positive -> Z
-fun x : positive => Zneg x~0
+fun x : positive => Z.neg x~0
      : positive -> Z
-fun x : positive => (Zpos x~0 + 0)%Z
+fun x : positive => (Z.pos x~0 + 0)%Z
      : positive -> Z
-fun x : positive => (- Zpos x~0)%Z
+fun x : positive => (- Z.pos x~0)%Z
      : positive -> Z
-fun x : positive => (- Zpos x~0 + 0)%Z
+fun x : positive => (- Z.pos x~0 + 0)%Z
      : positive -> Z
 (Z.of_nat 0 + 1)%Z
      : Z