diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-26 16:57:26 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-26 16:57:26 +0000 |
| commit | 7e5ae3dc23fb4823f8ff8851a01023733fc056f8 (patch) | |
| tree | 93575dea82ce032348f82061230854301dc8aad5 /theories/Numbers | |
| parent | 781f9487907a301282b17452ad8cf596077cd896 (diff) | |
Even better test for choosing rewrite or setoid_rewrite.
Now there is a class "SetoidRelation" for registering relations that
should always be considered as setoids and never unfolded. Every "Add
Relation" command adds an instance and impl,iff are there by
default. Now the test is: if there is a SetoidRelation instance, use it
; otherwise, allow unfolding to find an eq or fallback on
setoid_rewrite. To avoid searching for SetoidRelation instances
repeateadly we check that it is really needed first by unfolding the
hyp. Only two scripts relied on the now-forbidden semantics of rewriting
by an @eq inside a setoid relation, in Numbers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11269 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index e1f04e45a..4d1054553 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -216,7 +216,7 @@ Qed. Add Morphism Z.compare with signature Z.eq ==> Z.eq ==> (@eq comparison) as compare_wd. Proof. intros x x' Hx y y' Hy. -rewrite 2 spec_compare_alt; rewrite Hx, Hy; intuition. +rewrite 2 spec_compare_alt; unfold Z.eq in *; rewrite Hx, Hy; intuition. Qed. Add Morphism Z.lt with signature Z.eq ==> Z.eq ==> iff as NZlt_wd. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 4f558e80a..d5cb2882c 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -223,7 +223,7 @@ Qed. Add Morphism N.compare with signature N.eq ==> N.eq ==> (@eq comparison) as compare_wd. Proof. intros x x' Hx y y' Hy. -rewrite 2 spec_compare_alt; rewrite Hx, Hy; intuition. +rewrite 2 spec_compare_alt. unfold N.eq in *. rewrite Hx, Hy; intuition. Qed. Add Morphism N.lt with signature N.eq ==> N.eq ==> iff as NZlt_wd. |