diff options
| author | msozeau | 2008-03-08 19:45:09 +0000 |
|---|---|---|
| committer | msozeau | 2008-03-08 19:45:09 +0000 |
| commit | 311b326b3e3a317cfd309e17dafc8e77e6def49b (patch) | |
| tree | 07288fd75692a847cf11c0edfc09c9146bf0168a /test-suite | |
| parent | 329dcbec0e950f58334ec46938d7d74ad73cb617 (diff) | |
New implementation of Add Relation as a DefaultRelation instance
declaration. Really fix bug#1704, correct order of condition subgoals
even in setoid_rewrite.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10642 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/setoid_test.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 2be1500f4e..a7818f6f6d 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -110,7 +110,7 @@ Definition id: Set -> Set := fun A => A. Definition rel : forall A : Set, relation (id A) := @eq. Definition f: forall A : Set, A -> A := fun A x => x. -Instance DefaultRelation (id A) (rel A). +Add Relation (id A) (rel A) as eq_rel. Add Morphism (@f A) : f_morph. Proof. |