diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-28 14:53:00 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-28 14:53:00 +0000 |
| commit | ee711f8994d5e2e94cc61292ac6aab125c23df1c (patch) | |
| tree | ac25d186d1c280327dfa7654ff1dd8929b942d76 /theories/Numbers/Cyclic/Abstract | |
| parent | 94dc370fac30092d68b4d1aeb91ad9380232dbc2 (diff) | |
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
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 2 | ||||
| -rw-r--r-- | 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 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. |