Reverted 13293 commited mistakenly. Sorry for the noise.

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

2 files changed, 22 insertions, 22 deletions

diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index a8b5576f54..2dce5fbe4a 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -100,8 +100,8 @@ Section decidability.
 
   Definition Z_le_gt_dec : {x <= y} + {x > y}.
   Proof.
-    elim Z_le_dec; auto.
-    intro. right. apply Znot_le_gt; auto.
+    elim Z_le_dec; auto with arith.
+    intro. right. apply Znot_le_gt; auto with arith.
   Defined.
 
   Definition Z_gt_le_dec : {x > y} + {x <= y}.
@@ -111,17 +111,17 @@ Section decidability.
 
   Definition Z_ge_lt_dec : {x >= y} + {x < y}.
   Proof.
-    elim Z_ge_dec; auto.
-    intro. right. apply Znot_ge_lt; auto.
+    elim Z_ge_dec; auto with arith.
+    intro. right. apply Znot_ge_lt; auto with arith.
   Defined.
 
   Definition Z_le_lt_eq_dec : x <= y -> {x < y} + {x = y}.
   Proof.
     intro H.
     apply Zcompare_rec with (n := x) (m := y).
-    intro. right. elim (Zcompare_Eq_iff_eq x y); auto.
-    intro. left. elim (Zcompare_Eq_iff_eq x y); auto.
-    intro H1. absurd (x > y); auto.
+    intro. right. elim (Zcompare_Eq_iff_eq x y); auto with arith.
+    intro. left. elim (Zcompare_Eq_iff_eq x y); auto with arith.
+    intro H1. absurd (x > y); auto with arith.
   Defined.
 
 End decidability.
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 0c87f62234..4dfce35cec 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -145,32 +145,32 @@ Definition Zdiv2 (z:Z) :=
 Lemma Zeven_div2 : forall n:Z, Zeven n -> n = 2 * Zdiv2 n.
 Proof.
   intro x; destruct x.
-  auto.
-  destruct p; auto.
-  intros. absurd (Zeven (Zpos (xI p))); red in |- *; auto.
-  intros. absurd (Zeven 1); red in |- *; auto.
-  destruct p; auto.
-  intros. absurd (Zeven (Zneg (xI p))); red in |- *; auto.
-  intros. absurd (Zeven (-1)); red in |- *; auto.
+  auto with arith.
+  destruct p; auto with arith.
+  intros. absurd (Zeven (Zpos (xI p))); red in |- *; auto with arith.
+  intros. absurd (Zeven 1); red in |- *; auto with arith.
+  destruct p; auto with arith.
+  intros. absurd (Zeven (Zneg (xI p))); red in |- *; auto with arith.
+  intros. absurd (Zeven (-1)); red in |- *; auto with arith.
 Qed.
 
 Lemma Zodd_div2 : forall n:Z, n >= 0 -> Zodd n -> n = 2 * Zdiv2 n + 1.
 Proof.
   intro x; destruct x.
-  intros. absurd (Zodd 0); red in |- *; auto.
-  destruct p; auto.
-  intros. absurd (Zodd (Zpos (xO p))); red in |- *; auto.
-  intros. absurd (Zneg p >= 0); red in |- *; auto.
+  intros. absurd (Zodd 0); red in |- *; auto with arith.
+  destruct p; auto with arith.
+  intros. absurd (Zodd (Zpos (xO p))); red in |- *; auto with arith.
+  intros. absurd (Zneg p >= 0); red in |- *; auto with arith.
 Qed.
 
 Lemma Zodd_div2_neg :
   forall n:Z, n <= 0 -> Zodd n -> n = 2 * Zdiv2 n - 1.
 Proof.
   intro x; destruct x.
-  intros. absurd (Zodd 0); red in |- *; auto.
-  intros. absurd (Zneg p >= 0); red in |- *; auto.
-  destruct p; auto.
-  intros. absurd (Zodd (Zneg (xO p))); red in |- *; auto.
+  intros. absurd (Zodd 0); red in |- *; auto with arith.
+  intros. absurd (Zneg p >= 0); red in |- *; auto with arith.
+  destruct p; auto with arith.
+  intros. absurd (Zodd (Zneg (xO p))); red in |- *; auto with arith.
 Qed.
 
 Lemma Z_modulo_2 :