option -dump-glob pour coqdoc

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

1 files changed, 5 insertions, 7 deletions

diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index 593555586..5f1d6ba47 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -13,10 +13,10 @@ Require zarith_aux.
 Require auxiliary.
 Require Zsyntax.
 
-(* Our purpose is to write an induction shema for {0,1,2,...}
-  similar to the nat schema (Theorem [Natlike_rec]). For that the
+(** Our purpose is to write an induction shema for {0,1,2,...}
+  similar to the [nat] schema (Theorem [Natlike_rec]). For that the
   following implications will be used :
-\begin{verbatim}
+<<
  (n:nat)(Q n)==(n:nat)(P (inject_nat n)) ===> (x:Z)`x > 0) -> (P x)
 
        	     /\
@@ -28,10 +28,8 @@ Require Zsyntax.
       	       	       	       	<=== (inject_nat (S n))=(Zs (inject_nat n))
 
       	       	       	       	<=== inject_nat_complete
-
-  Then the  diagram will be closed and the theorem proved. 
-\end{verbatim}
-*)
+>>
+  Then the  diagram will be closed and the theorem proved. *)
 
 Lemma inject_nat_complete :
   (x:Z)`0 <= x` -> (EX n:nat | x=(inject_nat n)).