Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc,

et une typo dans Eqdep_deq.v



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

2 files changed, 3 insertions, 4 deletions

diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 3c276cd2bc..ba183b1f85 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -236,7 +236,7 @@ Module DecidableEqDep (M:DecidableType).
 End DecidableEqDep.
 
 (************************************************************************)
-(** ** B Definition of the functor that builds properties of dependent equalities on decidable sets in Set *)
+(** ** Definition of the functor that builds properties of dependent equalities on decidable sets in Set *)
 
 (** The signature of decidable sets in [Set] *)
 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index a095e9d137..b5098e6918 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -461,9 +461,8 @@ and doc_bol = parse
   | space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')?
       { let eol, lex = strip_eol (lexeme lexbuf) in
         let lev, s = sec_title lex in
-Printf.eprintf "%s %d" s (if eol then 1 else 2);
-        section lev (fun () -> ignore (doc (from_string s)));
-	if eol then doc_bol lexbuf else doc lexbuf }
+          section lev (fun () -> ignore (doc (from_string s)));
+	  if eol then doc_bol lexbuf else doc lexbuf }
   | space* '-'+
       { let n = count_dashes (lexeme lexbuf) in
 	if n >= 4 then rule () else item n;