diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-13 00:38:28 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-13 00:38:28 +0000 |
| commit | c242a71f206dfbafff457a1229b6322172d64f55 (patch) | |
| tree | 9248af1dfe5b8cd8dfafd37aa31043ea840aa2fb /test-suite/bugs/closed | |
| parent | 0024fe475225340d652d15e68d1e4f657d76cc08 (diff) | |
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
Diffstat (limited to 'test-suite/bugs/closed')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1784.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2083.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2139.v | 2 |
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 8c2e50e07..51d5ca728 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 6fc046495..a6ce4de0f 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 415a1b27d..a7f355088 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 ? *) - |