diff options
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. |