Rewrite of Program Fixpoint to overcome the previous limitations:

- The measure can now refer to all the formal arguments
- The recursive calls can make all the arguments vary as well
- Generalized to any relation and measure (new syntax {measure m on R})
This relies on an automatic curryfication transformation, the real
fixpoint combinator is working on a sigma type of the arguments. 
Reduces to the previous impl in case only one argument is involved.
The patch also introduces a new flag on implicit arguments that says if
the argument has to be infered (default) or can be turned into a
subgoal/obligation. Comes with a test-suite file.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12030 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 2 deletions

diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index e1e334be6..3a57fd545 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -57,6 +57,9 @@ END
 
 (* Errors *)
 
+let error_expect_two_arguments loc =
+  user_err_loc (loc,"",str "wrong number of arguments (expect two).")
+
 let error_expect_one_argument loc =
   user_err_loc (loc,"",str "wrong number of arguments (expect one).")
 
@@ -241,8 +244,8 @@ and interp_xml_recursionOrder x =
 	     | _ -> error_expect_one_argument loc)
       | "Measure" -> 
 	  (match l with
-	       [c] -> RMeasureRec (interp_xml_type c)
-	     | _ -> error_expect_one_argument loc)
+	       [m;r] -> RMeasureRec (interp_xml_type m, Some (interp_xml_type r))
+	     | _ -> error_expect_two_arguments loc)
       | _ ->
           user_err_loc (locs,"",str "Invalid recursion order.")