2 files changed, 13 insertions, 13 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.