diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-08 14:52:02 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-08 14:52:02 +0000 |
| commit | 6164aabc75035ca21474b51ceab4e25d47395ff7 (patch) | |
| tree | ebbd1dacc3ee8feb9c86a1e8edf6518ae8cf5e86 /test-suite/success/setoid_test2.v | |
| parent | 16ae29315ae0f88c4926b97f8fe22bffe65aa3e1 (diff) | |
Fix bugs that were reopened due to the change of setoid
implementation. Mostly syntax changes when declaring parametric
relations, but also some declarations were relying on "default"
relations on some carrier. Added a new DefaultRelation type class that
allows to do that, falling back to the last declared Equivalence
relation by default. This will be bound to Add Relation in the next
commit.
Also, move the "left" and "right" notations in Program.Utils to "in_left" and
"in_right" to avoid clashes with existing scripts.
Minor change to record to allow choosing the name of the argument for
the record in projections to avoid possible incompatibilities.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10639 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/setoid_test2.v')
| -rw-r--r-- | test-suite/success/setoid_test2.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v index bac1cf149..8e5729dce 100644 --- a/test-suite/success/setoid_test2.v +++ b/test-suite/success/setoid_test2.v @@ -120,6 +120,8 @@ Axiom eqS1: S1 -> S1 -> Prop. Axiom SetoidS1 : Setoid_Theory S1 eqS1. Add Setoid S1 eqS1 SetoidS1 as S1setoid. +Instance DefaultRelation S1 eqS1. + Axiom eqS1': S1 -> S1 -> Prop. Axiom SetoidS1' : Setoid_Theory S1 eqS1'. Axiom SetoidS1'_bis : Setoid_Theory S1 eqS1'. @@ -218,6 +220,8 @@ Axiom eqS1_test8: S1_test8 -> S1_test8 -> Prop. Axiom SetoidS1_test8 : Setoid_Theory S1_test8 eqS1_test8. Add Setoid S1_test8 eqS1_test8 SetoidS1_test8 as S1_test8setoid. +Instance DefaultRelation S1_test8 eqS1_test8. + Axiom f_test8 : S2 -> S1_test8. Add Morphism f_test8 : f_compat_test8. Admitted. |