From 02699217340a08f9ac7e6cef8650246d730f9624 Mon Sep 17 00:00:00 2001 From: msozeau Date: Sun, 29 Mar 2009 10:26:26 +0000 Subject: 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 --- test-suite/bugs/closed/shouldsucceed/2083.v | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'test-suite/bugs/closed') 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. -- cgit v1.2.3