From ee711f8994d5e2e94cc61292ac6aab125c23df1c Mon Sep 17 00:00:00 2001
From: glondu
Date: Mon, 28 Jun 2010 14:53:00 +0000
Subject: Fix compilation by replacing some "auto with zarith" with "ring"

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13212 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 2 +-
 theories/Numbers/Cyclic/Abstract/NZCyclic.v     | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 0403722cb3..1e66d9b9ef 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -269,7 +269,7 @@ Module ZnZ.
  case (of_pos p); intros n w1; simpl.
  case n; simpl Npos; auto with zarith.
  intros p1 Hp1; contradict Hp; apply Zle_not_lt.
- replace (base digits) with (1 * base digits + 0) by auto with zarith.
+ replace (base digits) with (1 * base digits + 0) by ring.
  rewrite Hp1.
  apply Zplus_le_compat.
  apply Zmult_le_compat; auto with zarith.
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 0796d9f49b..1149bc2cdd 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -100,7 +100,7 @@ Theorem pred_succ : forall n, P (S n) == n.
 Proof.
 intro n. zify.
 rewrite <- pred_mod_wB.
-replace ([| n |] + 1 - 1)%Z with [| n |] by auto with zarith. apply NZ_to_Z_mod.
+replace ([| n |] + 1 - 1)%Z with [| n |] by ring. apply NZ_to_Z_mod.
 Qed.
 
 Section Induction.
@@ -170,7 +170,7 @@ Theorem sub_succ_r : forall n m, n - (S m) == P (n - m).
 Proof.
 intros n m. zify. rewrite Zminus_mod_idemp_r, Zminus_mod_idemp_l.
 now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z
-     by auto with zarith.
+     by ring.
 Qed.
 
 Theorem mul_0_l : forall n, 0 * n == 0.
-- 
cgit v1.2.3