From f89818edb6fd0e66aebee3b7ac13b4b263252a63 Mon Sep 17 00:00:00 2001
From: emakarov
Date: Thu, 8 Nov 2007 22:27:31 +0000
Subject: 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
---
 theories/Arith/Wf_nat.v | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index 7e85e5c67b..6e8f154c73 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 : 
-- 
cgit v1.2.3