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

1 files changed, 7 insertions, 7 deletions

diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index a8b5576f5..2dce5fbe4 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.