3 files changed, 6 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
index 8c2e50e07d..51d5ca728a 100644
--- a/test-suite/bugs/closed/shouldsucceed/1784.v
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -93,9 +93,9 @@ Next Obligation.
   intro H1; contradict H. inversion H1; subst. assumption.
   contradict H0; assumption. Defined.
 Next Obligation.
-  intro H1; contradict H0. inversion H1; subst. assumption. Defined.
+  intro H1; contradict H. inversion H1; subst. assumption. Defined.
 Next Obligation.
-  intro H0; contradict H. inversion H0; subst. assumption. Defined.
+  intro H1; contradict H0. inversion H1; subst. assumption. Defined.
 Next Obligation.
   intro H0; contradict H. inversion H0; subst; auto. Defined.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/2083.v b/test-suite/bugs/closed/shouldsucceed/2083.v
index 6fc046495c..a6ce4de0f6 100644
--- a/test-suite/bugs/closed/shouldsucceed/2083.v
+++ b/test-suite/bugs/closed/shouldsucceed/2083.v
@@ -15,11 +15,13 @@ Program Fixpoint check_n  (n : nat) (P : { i | i < n } -> bool) (p : nat)
 
 Require Import Omega.
 
+Solve Obligations using program_simpl ; auto with *; try omega.
+
 Next Obligation.
   apply H. simpl. omega.
 Defined.
 
-Next Obligation.
+Next Obligation. 
   case (le_lt_dec p i) ; intros. assert(i = p) by omega. subst.
   revert H0. clear_subset_proofs. auto.
   apply H. simpl. assumption. Defined.
diff --git a/test-suite/bugs/closed/shouldsucceed/2139.v b/test-suite/bugs/closed/shouldsucceed/2139.v
index 415a1b27dd..a7f3550888 100644
--- a/test-suite/bugs/closed/shouldsucceed/2139.v
+++ b/test-suite/bugs/closed/shouldsucceed/2139.v
@@ -1,4 +1,5 @@
 (* Call of apply on <-> failed because of evars in elimination predicate *)
+Generalizable Variables patch.
 
 Class Patch (patch : Type) := {
     commute : patch -> patch -> Prop
@@ -21,4 +22,3 @@ apply flip in H.
    type of (@flip _ _ _ _) itself had non-normalized evars *)
 
 (* By the way, is the check necessary ? *)
-