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

3 files changed, 6 insertions, 13 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 9152083bf3..66fc4c2532 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -398,7 +398,7 @@ GEXTEND Gram
     [ [ "{"; IDENT "struct"; id=identref; "}" -> (Some id, CStructRec)
     | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> (id, CWfRec rel)
     | "{"; IDENT "measure"; m=constr; id=OPT identref; 
-	rel = OPT [ "on"; r=constr -> r ]; "}" -> (id, CMeasureRec (m,rel))
+	rel=OPT constr; "}" -> (id, CMeasureRec (m,rel))
     ] ]
   ;
   binders_let_fixannot:
diff --git a/test-suite/bugs/closed/shouldsucceed/2083.v b/test-suite/bugs/closed/shouldsucceed/2083.v
index 3e2d00cbad..63f91e5658 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.
diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
index 8cf97b03fa..1898853f61 100644
--- a/test-suite/success/ProgramWf.v
+++ b/test-suite/success/ProgramWf.v
@@ -3,8 +3,9 @@ Set Implicit Arguments.
 (* Set Printing All. *)
 Print sigT_rect.
 Obligation Tactic := program_simplify ; auto with *.
+About MR.
 
-Program Fixpoint merge (n m : nat) {measure (n + m) on lt} : nat :=
+Program Fixpoint merge (n m : nat) {measure (n + m) (lt)} : nat :=
   match n with
     | 0 => 0
     | S n' => merge n' m
@@ -21,7 +22,7 @@ Print Zwf.
 
 Open Local Scope Z_scope.
 
-Program Fixpoint Zwfrec (n m : Z) {measure (n + m) on (Zwf 0)} : Z :=
+Program Fixpoint Zwfrec (n m : Z) {measure (n + m) (Zwf 0)} : Z :=
   match n ?= m with
     | Lt => Zwfrec n (Zpred m)
     | _ => 0
@@ -91,13 +92,7 @@ Next Obligation. simpl in *; intros.
   apply H. simpl. omega.
 Qed.
 
-Print check_n.
-Print sigT_rect.
-Print check_n.
-
 Program Fixpoint check_n'  (n : nat) (m : nat | m = n) (p : nat) (q : nat | q = p)
   {measure (p - n) p} : nat :=
   _.
 
-Print Opaque Dependencies check_n.
-