option -dump-glob pour coqdoc

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

5 files changed, 26 insertions, 22 deletions

diff --git a/theories/IntMap/Adalloc.v b/theories/IntMap/Adalloc.v
index ab7f19a07f..8fe68376bf 100644
--- a/theories/IntMap/Adalloc.v
+++ b/theories/IntMap/Adalloc.v
@@ -188,7 +188,7 @@ Section AdAlloc.
     Intro H0. Rewrite H0 in H. Assumption.
   Qed.
 
-  (* Allocator: returns an address not in the domain of m.
+  (** Allocator: returns an address not in the domain of [m].
   This allocator is optimal in that it returns the lowest possible address,
   in the usual ordering on integers. It is not the most efficient, however. *)
   Fixpoint ad_alloc_opt [m:(Map A)] : ad :=
@@ -221,8 +221,8 @@ Section AdAlloc.
     Unfold in_dom. Intro. Rewrite (ad_alloc_opt_allocates_1 m). Reflexivity.
   Qed.
 
-  (* Moreover, this is optimal: all addresses below [(ad_alloc_opt m)]
-     are in [dom m]: *)
+  (** Moreover, this is optimal: all addresses below [(ad_alloc_opt m)]
+      are in [dom m]: *)
 
   Lemma convert_xH : (convert xH)=(1).
   Proof.
diff --git a/theories/IntMap/Addec.v b/theories/IntMap/Addec.v
index 64c5337288..17742d60c4 100644
--- a/theories/IntMap/Addec.v
+++ b/theories/IntMap/Addec.v
@@ -7,7 +7,8 @@
 (***********************************************************************)
 (*i 	$Id$	 i*)
 
-(*s Equality on adresses *)
+(** Equality on adresses *)
+
 Require Bool.
 Require Sumbool.
 Require ZArith.
diff --git a/theories/IntMap/Addr.v b/theories/IntMap/Addr.v
index a74dcf5b87..435a7c21c3 100644
--- a/theories/IntMap/Addr.v
+++ b/theories/IntMap/Addr.v
@@ -7,7 +7,7 @@
 (***********************************************************************)
 (*i 	$Id$	 i*)
 
-(*s Representation of adresses by the [positive] type of binary numbers *)
+(** Representation of adresses by the [positive] type of binary numbers *)
 
 Require Bool.
 Require ZArith.
diff --git a/theories/IntMap/Adist.v b/theories/IntMap/Adist.v
index 0361b12c80..5c3296885c 100644
--- a/theories/IntMap/Adist.v
+++ b/theories/IntMap/Adist.v
@@ -237,15 +237,17 @@ Proof.
 Qed.
 
 
-(*s We define an ultrametric distance between addresses: $d(a,a')=1/2^pd(a,a')$,
-  where $pd(a,a')$ is the number of identical bits at the beginning of $a$ and $a'$
-  (infinity if $a=a'$).  Instead of working with $d$, we work with $pd$, namely
-  [ad_pdist]: *)
+(** We define an ultrametric distance between addresses: 
+    $d(a,a')=1/2^pd(a,a')$, 
+    where $pd(a,a')$ is the number of identical bits at the beginning 
+    of $a$ and $a'$ (infinity if $a=a'$).  
+    Instead of working with $d$, we work with $pd$, namely
+    [ad_pdist]: *)
 
 Definition ad_pdist := [a,a':ad] (ad_plength (ad_xor a a')).
 
-(*s d is a distance, so $d(a,a')=0$ iff $a=a'$; this means that
-  $pd(a,a')=infty$ iff $a=a'$: *)
+(** d is a distance, so $d(a,a')=0$ iff $a=a'$; this means that
+    $pd(a,a')=infty$ iff $a=a'$: *)
 
 Lemma ad_pdist_eq_1 : (a:ad) (ad_pdist a a)=infty.
 Proof.
@@ -257,14 +259,15 @@ Proof.
   Intros. Apply ad_xor_eq. Apply ad_plength_infty. Exact H.
 Qed.
 
-(*s $d$ is a distance, so $d(a,a')=d(a',a)$: *)
+(** $d$ is a distance, so $d(a,a')=d(a',a)$: *)
 
 Lemma ad_pdist_comm : (a,a':ad) (ad_pdist a a')=(ad_pdist a' a).
 Proof.
   Unfold ad_pdist. Intros. Rewrite ad_xor_comm. Reflexivity.
 Qed.
 
-(*s $d$ is an ultrametric distance, that is, not only $d(a,a')\leq d(a,a'')+d(a'',a')$,
+(** $d$ is an ultrametric distance, that is, not only $d(a,a')\leq
+    d(a,a'')+d(a'',a')$,
   but in fact $d(a,a')\leq max(d(a,a''),d(a'',a'))$.
   This means that $min(pd(a,a''),pd(a'',a'))<=pd(a,a')$ (lemma [ad_pdist_ultra] below).
   This follows from the fact that $a \Ra |a| = 1/2^{\texttt{ad\_plength}}(a))$
diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v
index 245ceb558e..b89f610421 100644
--- a/theories/IntMap/Map.v
+++ b/theories/IntMap/Map.v
@@ -7,7 +7,7 @@
 (***********************************************************************)
 (*i 	$Id$	 i*)
 
-(*s Definition of finite sets as trees indexed by adresses *)
+(** Definition of finite sets as trees indexed by adresses *)
 
 Require Bool.
 Require Sumbool.
@@ -19,7 +19,7 @@ Require Addec.
 
 Section MapDefs.
 
-(*s We define maps from ad to A. *)
+(** We define maps from ad to A. *)
   Variable A : Set.  
 
   Inductive Map : Set :=
@@ -37,9 +37,9 @@ Section MapDefs.
     Left . Split with a. Reflexivity.
   Qed.
 
-  (* The semantics of maps is given by the function MapGet.
-    The semantics of a map m is a partial, finite function from
-    ad to A: *)
+  (** The semantics of maps is given by the function [MapGet].
+      The semantics of a map [m] is a partial, finite function from
+      [ad] to [A]: *)
 
   Fixpoint MapGet [m:Map] : ad -> option :=
     Cases m of
@@ -604,8 +604,8 @@ Section MapDefs.
     Reflexivity.
   Qed.
 
-  (* MapInter, MapRngRestrTo, MapRngRestrBy, MapInverse not implemented:
-     need a decidable equality on A. *)
+  (** [MapInter], [MapRngRestrTo], [MapRngRestrBy], [MapInverse] 
+      not implemented: need a decidable equality on [A]. *)
 
   Fixpoint MapDelta [m:Map] : Map -> Map :=
     Cases m of
@@ -780,7 +780,7 @@ Section MapDefs.
     Intros. Discriminate H1.
   Qed.
 
-  (* MapSplit not implemented: not the preferred way of recursing over Maps
-  (use MapSweep, MapCollect, or MapFold in Mapiter.v. *)
+  (** [MapSplit] not implemented: not the preferred way of recursing over Maps
+      (use [MapSweep], [MapCollect], or [MapFold] in Mapiter.v. *)
 
 End MapDefs.