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

7 files changed, 32 insertions, 28 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1634.v b/test-suite/bugs/closed/shouldsucceed/1634.v
index 9e50f6f252..205e827982 100644
--- a/test-suite/bugs/closed/shouldsucceed/1634.v
+++ b/test-suite/bugs/closed/shouldsucceed/1634.v
@@ -3,22 +3,22 @@ Require Export Setoid.
 
 Variable A : Type.
 Variable S : A -> Type.
-Variable Seq : forall (a:A), relation (S a).
+Variable Seq : forall {a:A}, relation (S a).
 
-Hypothesis Seq_refl : forall (a:A) (x : S a), Seq a x x.
-Hypothesis Seq_sym : forall (a:A) (x y : S a), Seq a x y -> Seq a y x.
-Hypothesis Seq_trans : forall (a:A) (x y z : S a), Seq a x y -> Seq a y z ->
-Seq
-a x z.
+Hypothesis Seq_refl : forall {a:A} (x : S a), Seq x x.
+Hypothesis Seq_sym : forall {a:A} (x y : S a), Seq x y -> Seq y x.
+Hypothesis Seq_trans : forall {a:A} (x y z : S a), Seq x y -> Seq y z ->
+Seq x z.
 
-Add Relation S Seq
+Add Relation (S a) Seq
  reflexivity proved by Seq_refl
  symmetry proved by Seq_sym
  transitivity proved by Seq_trans
  as S_Setoid.
 
-Goal forall (a : A) (x y : S a), Seq a x y -> Seq a x y.
+Goal forall (a : A) (x y : S a), Seq x y -> Seq x y.
   intros a x y H.
-  setoid_replace x with y using relation Seq.
-  apply Seq_refl. trivial.
+  setoid_replace x with y. 
+  reflexivity.
+  trivial.
 Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/846.v b/test-suite/bugs/closed/shouldsucceed/846.v
index a963b225fe..95bbab92a3 100644
--- a/test-suite/bugs/closed/shouldsucceed/846.v
+++ b/test-suite/bugs/closed/shouldsucceed/846.v
@@ -138,15 +138,15 @@ Proof.
   right; assumption.
   intros l _ r.
   apply (step (A:=L' A l)).
-  exact (inl _ (inl _ r)).
+  exact (inl (inl r)).
   intros l _ r1 _ r2.
   apply (step (A:=L' A l)).
   (* unfold L' in * |- *.
   Check 0. *)
-  exact (inl _ (inr _ (pair r1 r2))).
+  exact (inl (inr (pair r1 r2))).
   intros l _ r.
   apply  (step (A:=L' A l)).
-  exact (inr _ r).
+  exact (inr r).
 Defined.
 
 Definition L'inG: forall A: Set, L' A (true::nil) -> G A.
diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out
index cbfb9f207b..a24ad124eb 100644
--- a/test-suite/output/ZSyntax.out
+++ b/test-suite/output/ZSyntax.out
@@ -2,19 +2,19 @@
      : Z
 fun f : nat -> Z => (f 0%nat + 0)%Z
      : (nat -> Z) -> Z
-fun x : positive => Zpos (xO x)
+fun x : positive => Zpos x~0)
      : positive -> Z
 fun x : positive => (Zpos x + 1)%Z
      : positive -> Z
 fun x : positive => Zpos x
      : positive -> Z
-fun x : positive => Zneg (xO x)
+fun x : positive => Zneg x~0
      : positive -> Z
-fun x : positive => (Zpos (xO x) + 0)%Z
+fun x : positive => (Zpos x~0 + 0)%Z
      : positive -> Z
-fun x : positive => (- Zpos (xO x))%Z
+fun x : positive => (- Zpos x~0)%Z
      : positive -> Z
-fun x : positive => (- Zpos (xO x) + 0)%Z
+fun x : positive => (- Zpos x~0 + 0)%Z
      : positive -> Z
 (Z_of_nat 0 + 1)%Z
      : Z
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 0b3060d519..6a5bf58b64 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -84,7 +84,7 @@ Extraction test12.
 (* type test12 = (__ -> __ -> __) -> __ *)
 
 
-Definition test13 := match left True I with
+Definition test13 := match @left True True I with
                      | left x => 1
                      | right x => 0
                      end.
@@ -322,7 +322,7 @@ Extraction test24.
 Require Import Gt.
 Definition loop (Ax:Acc gt 0) :=
   (fix F (a:nat) (b:Acc gt a) {struct b} : nat :=
-     F (S a) (Acc_inv b (S a) (gt_Sn_n a))) 0 Ax.
+     F (S a) (Acc_inv b (gt_Sn_n a))) 0 Ax.
 Extraction loop.
 (* let loop _ =
   let rec f a =
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index e99b3c19bb..2be1500f4e 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -110,9 +110,9 @@ 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.
 
-Add Relation id rel as eq_rel.
+Instance DefaultRelation (id A) (rel A).
 
-Add Morphism f with signature rel ++> rel as f_morph.
+Add Morphism (@f A) : f_morph.
 Proof.
 unfold rel, f. trivial.
 Qed.
diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v
index bac1cf1493..8e5729dce0 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.
 
diff --git a/test-suite/success/setoid_test_function_space.v b/test-suite/success/setoid_test_function_space.v
index 1602991df2..2e9bd60ea7 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