From c242a71f206dfbafff457a1229b6322172d64f55 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 13 Nov 2009 00:38:28 +0000
Subject: Fix test-suite scripts: [Generalizable Variables] and small changes
 in obligations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12514 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/bugs/closed/shouldsucceed/1784.v | 4 ++--
 test-suite/bugs/closed/shouldsucceed/2083.v | 4 +++-
 test-suite/bugs/closed/shouldsucceed/2139.v | 2 +-
 3 files changed, 6 insertions(+), 4 deletions(-)

(limited to 'test-suite/bugs')

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 ? *)
-
-- 
cgit v1.2.3