Correction du bug #1814 (trunk et v8.1) + améliorations dans coqdep et coq_makefile

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

1 files changed, 6 insertions, 6 deletions

diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index db1caaeee5..8774d9d2e4 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -189,7 +189,7 @@ let symbolchar_no_brackets =
   '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _
 let symbolchar = symbolchar_no_brackets | '[' | ']'
 let token = symbolchar+ | '[' [^ '[' ']' ':']* ']'
-
+let printing_token = (token | id)+
 
 let thm_token = 
   "Theorem" 
@@ -370,9 +370,9 @@ rule coq_bol = parse
 	    let eol= body lexbuf in
 	      if eol then coq_bol lexbuf else coq lexbuf }
 
-  | space* "(**" space+ "printing" space+ (identifier | token) space+
+  | space* "(**" space+ "printing" space+ printing_token space+
       { let tok = lexeme lexbuf in
-	let s = printing_token lexbuf in
+	let s = printing_token_body lexbuf in
 	  add_printing_token tok s;
 	  coq_bol lexbuf }
   | space* "(**" space+ "printing" space+
@@ -617,7 +617,7 @@ and body = parse
       { let s = lexeme lexbuf in 
 	  Output.ident s (lexeme_start lexbuf); 
 	  body lexbuf }
-  | token
+  | printing_token
       { let s = lexeme lexbuf in
 	  Output.symbol s; body lexbuf }
   | _ { let c = lexeme_char lexbuf 0 in 
@@ -645,13 +645,13 @@ and skip_hide = parse
 
 (*s Reading token pretty-print *)
 
-and printing_token = parse
+and printing_token_body = parse
   | "*)" | eof 
 	{ let s = Buffer.contents token_buffer in 
 	  Buffer.clear token_buffer;
 	  s }
   | _   { Buffer.add_string token_buffer (lexeme lexbuf); 
-	  printing_token lexbuf }
+	  printing_token_body lexbuf }
 
 (*s Applying the scanners to files *)