From 311b326b3e3a317cfd309e17dafc8e77e6def49b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 8 Mar 2008 19:45:09 +0000
Subject: 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
---
 test-suite/success/setoid_test.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3