diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-29 10:26:26 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-29 10:26:26 +0000 |
| commit | 02699217340a08f9ac7e6cef8650246d730f9624 (patch) | |
| tree | 7e027b2fa46362a98a22da1c2f75ff99b9371264 /test-suite/bugs/closed/shouldsucceed/2083.v | |
| parent | 2d8aa8a39eaa4e44d9ece9fdfbcbf4bc4a516dec (diff) | |
Avoid inadvertent declaration of "on" as a keyword. New syntax is
{measure ms [id] [(rel)]}. Fix script of bug #2083 and test-suite file
accordingly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12032 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/2083.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2083.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2083.v b/test-suite/bugs/closed/shouldsucceed/2083.v index 3e2d00cba..63f91e565 100644 --- a/test-suite/bugs/closed/shouldsucceed/2083.v +++ b/test-suite/bugs/closed/shouldsucceed/2083.v @@ -1,15 +1,14 @@ Require Import Program Arith. -Set Implicit Arguments. Program Fixpoint check_n (n : nat) (P : { i | i < n } -> bool) (p : nat) (H : forall (i : { i | i < n }), i < p -> P i = true) - {measure (fun i => n - i) p} : + {measure (n - p)} : Exc (forall (p : { i | i < n}), P p = true) := match le_lt_dec n p with | left _ => value _ | right cmp => if dec (P p) then - check_n (S p) _ + check_n n P (S p) _ else error end. @@ -20,7 +19,6 @@ Next Obligation. apply H. simpl. omega. Defined. -Next Obligation. omega. Defined. Next Obligation. case (le_lt_dec p i) ; intros. assert(i = p) by omega. subst. revert H0. clear_subset_proofs. auto. |