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

2 files changed, 3 insertions, 3 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 0403722cb..1e66d9b9e 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 0796d9f49..1149bc2cd 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.