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