1 files changed, 10 insertions, 11 deletions

diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index f34c97d23f..16aa58afac 100755
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-(* Well-founded relations and natural numbers *)
+(** Well-founded relations and natural numbers *)
 
 Require Lt.
 
@@ -37,23 +37,22 @@ Qed.
 Theorem  well_founded_gtof : (well_founded A gtof).
 Proof well_founded_ltof.
 
-(* It is possible to directly prove the induction principle going
+(** It is possible to directly prove the induction principle going
    back to primitive recursion on natural numbers ([induction_ltof1])
    or to use the previous lemmas to extract a program with a fixpoint
    ([induction_ltof2]) 
-the ML-like program for [induction_ltof1] is :
-\begin{verbatim}
+
+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)));;
-\end{verbatim}
-the ML-like program for [induction_ltof2] is :
-\begin{verbatim}
+]]
+
+the ML-like program for [induction_ltof2] is : [[
    let induction_ltof2 F a = indrec a
    where rec indrec a = F a indrec;;
-\end{verbatim}
-*)
+]] *)
 
 Theorem induction_ltof1 
   : (P:A->Set)((x:A)((y:A)(ltof y x)->(P y))->(P x))->(a:A)(P a).
@@ -82,8 +81,8 @@ Theorem induction_gtof2
 Proof induction_ltof2.
 
 
-(* If a relation R is compatible with lt i.e. if x R y => f(x) < f(y)
-   then R is well-founded. *)
+(** If a relation [R] is compatible with [lt] i.e. if [x R y => f(x) < f(y)]
+    then [R] is well-founded. *)
 
 Variable R : A->A->Prop.