Fix setoid tests, use red for a Setoid_Theory lemma, and Parametric

Relation for function spaces.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10786 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 2 insertions, 2 deletions

diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index a7818f6f6d..f49f58e5a3 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -18,7 +18,7 @@ Definition same (s t : set) : Prop := forall a : A, In a s <-> In a t.
 
 Lemma setoid_set : Setoid_Theory set same.
 
-unfold same in |- *; split.
+unfold same in |- *; split ; red.
 red in |- *; auto.
 
 red in |- *.
diff --git a/test-suite/success/setoid_test_function_space.v b/test-suite/success/setoid_test_function_space.v
index 2e9bd60ea7..ead93d913a 100644
--- a/test-suite/success/setoid_test_function_space.v
+++ b/test-suite/success/setoid_test_function_space.v
@@ -26,7 +26,7 @@ Hint Unfold feq. Hint Resolve feq_refl feq_sym feq_trans.
 Variable K:(nat -> nat)->Prop.
 Variable K_ext:forall a b, (K a)->(a =f b)->(K b).
 
-Add Relation (A -> B) (@feq A B)
+Add Parametric Relation (A B : Type) : (A -> B) (@feq A B)
  reflexivity proved by (@feq_refl A B)
  symmetry proved by (@feq_sym A B)
  transitivity proved by (@feq_trans A B) as funsetoid.