Corrected the ML code for well-founded recursion in the comment.

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

1 files changed, 6 insertions, 4 deletions

diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 7e85e5c67..6e8f154c7 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -50,10 +50,12 @@ Defined.
 
 the ML-like program for [induction_ltof1] is : 
 [[
-   let induction_ltof1 F a = indrec ((f a)+1) a 
-   where rec indrec = 
-        function 0    -> (function a -> error)
-               |(S m) -> (function a -> (F a (function y -> indrec y m)));;
+let induction_ltof1 f F a =
+  let rec indrec n k =
+    match n with
+    | O -> error
+    | S m -> F k (indrec m)
+  in indrec (f a + 1) a
 ]]
 
 the ML-like program for [induction_ltof2] is :