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, 7 insertions, 11 deletions

diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index f1f73303a..c7e6a4f1d 100755
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -12,9 +12,7 @@ Require Export Plus.
 Require Export Minus.
 Require Export Lt.
 
-(**********************************************************)
-(* Multiplication                                         *)
-(**********************************************************)
+(** Multiplication *)
 
 Lemma mult_plus_distr : 
       (n,m,p:nat)((mult (plus n m) p)=(plus (mult n p) (mult m p))).
@@ -98,13 +96,11 @@ Proof.
   Apply mult_lt. Assumption.
 Qed.
 
-(**************************************************************************)
-(*                         Tail-recursive mult                            *)
-(**************************************************************************)
+(** Tail-recursive mult *)
 
-(* [tail_mult] is an alternative definition for [mult] which is 
-  tail-recursive, whereas [mult] is not. When extracting programs 
-  from proofs, this can be useful. *)
+(** [tail_mult] is an alternative definition for [mult] which is 
+    tail-recursive, whereas [mult] is not. This can be useful 
+    when extracting programs. *)
 
 Fixpoint mult_acc [s,m,n:nat] : nat := 
    Cases n of 
@@ -125,8 +121,8 @@ Lemma mult_tail_mult : (n,m:nat)(mult n m)=(tail_mult n m).
 Intros; Unfold tail_mult; Rewrite <- mult_acc_aux;Auto.
 Qed.
 
-(* [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus] 
-   and [mult] and simplify *)
+(** [TailSimpl] transforms any [tail_plus] and [tail_mult] into [plus] 
+    and [mult] and simplify *)
 
 Tactic Definition TailSimpl := 
    Repeat Rewrite <- plus_tail_plus;