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

1 files changed, 6 insertions, 6 deletions

diff --git a/test-suite/success/setoid_test_function_space.v b/test-suite/success/setoid_test_function_space.v
index 1602991df..2e9bd60ea 100644
--- a/test-suite/success/setoid_test_function_space.v
+++ b/test-suite/success/setoid_test_function_space.v
@@ -26,14 +26,14 @@ 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 (fun A B:Type => A -> B) feq
- reflexivity proved by feq_refl
- symmetry proved by feq_sym
- transitivity proved by feq_trans as funsetoid.
+Add Relation (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.
                                                                              
-Add Morphism K with signature feq ==> iff as K_ext1.
+Add Morphism K with signature (@feq nat nat) ==> iff as K_ext1.
 intuition. apply (K_ext H0 H).
-intuition. assert (x2 =f x1);auto.  apply (K_ext H0 H1).
+intuition. assert (y =f x);auto.  apply (K_ext H0 H1).
 Qed.
 
 Lemma three:forall n, forall a, (K a)->(a =f (fun m => (a (n+m))))-> (K (fun m