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

diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 275712084..44311a127 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -8,13 +8,12 @@
 
 (*i $Id$ i*)
 
-(* Here are collected some results about the type sumbool (see INIT/Specif.v)
- * [sumbool A B], which is written [{A}+{B}], is the informative
- * disjunction "A or B", where A and B are logical propositions.
- * Its extraction is isomorphic to the type of booleans.
- *)
+(** Here are collected some results about the type sumbool (see INIT/Specif.v)
+   [sumbool A B], which is written [{A}+{B}], is the informative
+   disjunction "A or B", where A and B are logical propositions.
+   Its extraction is isomorphic to the type of booleans. *)
 
-(* A boolean is either true or false, and this is decidable *)
+(** A boolean is either [true] or [false], and this is decidable *)
 
 Lemma sumbool_of_bool : (b:bool) {b=true}+{b=false}.
 Proof.
@@ -36,7 +35,7 @@ Save.
 
 (*i pourquoi ce machin-la est dans BOOL et pas dans LOGIC ?  Papageno i*)
 
-(* Logic connectives on type sumbool *)
+(** Logic connectives on type [sumbool] *)
 
 Section connectives.