diff options
| author | msozeau | 2008-03-07 16:32:12 +0000 |
|---|---|---|
| committer | msozeau | 2008-03-07 16:32:12 +0000 |
| commit | ec850ff623801e514b3ed0a42beb6f7984992520 (patch) | |
| tree | 6a03dd3d0545b927326f28e7d8da08a850cead5f /theories/Ints | |
| parent | 905c47d6a07cc69b9e7aa0b9d73caeacf2b1d2be (diff) | |
Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part
of the fix I added an optional "by" annotation for rewrite to solve said
conditions in the same tactic call. Most of the theories have been
updated, only FSets is missing, Pierre will take care of it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10634 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Ints')
| -rw-r--r-- | theories/Ints/num/QvMake.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Ints/num/QvMake.v b/theories/Ints/num/QvMake.v index e51291a041..c3db44bc6f 100644 --- a/theories/Ints/num/QvMake.v +++ b/theories/Ints/num/QvMake.v @@ -429,8 +429,8 @@ Module Qv. Theorem spec_sub x y: wf x -> wf y -> ([sub x y] == [x] - [y])%Q. intros x y Hx Hy; unfold sub; rewrite spec_add; auto. - apply wf_opp; auto. rewrite spec_opp; ring. + apply wf_opp; auto. Qed. Theorem spec_subc x y: wf x -> wf y -> @@ -450,8 +450,8 @@ Module Qv. Theorem spec_sub_norm x y: wf x -> wf y -> ([sub_norm x y] == [x] - [y])%Q. intros x y Hx Hy; unfold sub_norm; rewrite spec_add_norm; auto. - apply wf_opp; auto. rewrite spec_opp; ring. + apply wf_opp; auto. Qed. Theorem spec_sub_normc x y: wf x -> wf y -> @@ -945,10 +945,10 @@ Module Qv. Theorem spec_div x y: wf x -> wf y -> ([div x y] == [x] / [y])%Q. intros x y Hx Hy; unfold div; rewrite spec_mul; auto. - apply wf_inv; auto. unfold Qdiv; apply Qmult_comp. apply Qeq_refl. apply spec_inv; auto. + apply wf_inv; auto. Qed. Theorem spec_divc x y: wf x -> wf y -> @@ -969,10 +969,10 @@ Module Qv. Theorem spec_div_norm x y: wf x -> wf y -> ([div_norm x y] == [x] / [y])%Q. intros x y Hx Hy; unfold div_norm; rewrite spec_mul_norm; auto. - apply wf_inv; auto. unfold Qdiv; apply Qmult_comp. apply Qeq_refl. apply spec_inv; auto. + apply wf_inv; auto. Qed. Theorem spec_div_normc x y: wf x -> wf y -> |