3 files changed, 10 insertions, 9 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1411.v b/test-suite/bugs/closed/shouldsucceed/1411.v
index bb475bdc2a..e330d46fd1 100644
--- a/test-suite/bugs/closed/shouldsucceed/1411.v
+++ b/test-suite/bugs/closed/shouldsucceed/1411.v
@@ -1,4 +1,5 @@
 Require Import List.
+Require Import Program.
 
 Inductive Tree : Set :=
 | Br : Tree -> Tree -> Tree
diff --git a/test-suite/bugs/closed/shouldsucceed/1634.v b/test-suite/bugs/closed/shouldsucceed/1634.v
index 205e827982..e0c540f36e 100644
--- a/test-suite/bugs/closed/shouldsucceed/1634.v
+++ b/test-suite/bugs/closed/shouldsucceed/1634.v
@@ -10,7 +10,7 @@ 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 a) Seq
+Add Parametric Relation a : (S a) Seq
  reflexivity proved by Seq_refl
  symmetry proved by Seq_sym
  transitivity proved by Seq_trans
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
index 12c92a8f7f..d6b7660b2d 100644
--- a/test-suite/bugs/closed/shouldsucceed/1784.v
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -85,17 +85,17 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
       end
   end.
 
-Next Obligation. intro; apply H; inversion H0; subst; trivial. Defined.
-Next Obligation. intro; inversion H. Defined.
-Next Obligation. intro H; inversion H. Defined.
-Next Obligation. intro; inversion H; subst. Defined.
+Next Obligation. apply H; inversion H0; subst; trivial. reflexivity. Defined.
+Next Obligation. inversion H. Defined.
+Next Obligation. inversion H. Defined.
+Next Obligation. inversion H; subst. Defined.
 Next Obligation.
-  contradict H. inversion H; subst. assumption. 
+  contradict H. inversion H1; subst. assumption. 
   contradict H0; assumption. Defined.
 Next Obligation.
-  contradict H0. inversion H0; subst. assumption. Defined.
+  contradict H0. inversion H1; subst. assumption. Defined.
 Next Obligation.
-  contradict H. inversion H; subst. assumption. Defined.
+  contradict H. inversion H0; subst. assumption. Defined.
 Next Obligation.
-  contradict H. inversion H; subst; auto. Defined.
+  contradict H. inversion H0; subst; auto. Defined.