From bf342ae13354b715ac55bab3de8d7aea64c6dc52 Mon Sep 17 00:00:00 2001
From: notin
Date: Thu, 21 Jun 2007 17:51:01 +0000
Subject: 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
---
 theories/Logic/Eqdep_dec.v | 2 +-
 tools/coqdoc/pretty.mll    | 5 ++---
 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;
-- 
cgit v1.2.3