aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authornotin2006-03-25 13:22:09 +0000
committernotin2006-03-25 13:22:09 +0000
commitebcb2063bba0f87ef146b20357a4866fe8d0d4b0 (patch)
tree3ea4e54f15d15e1e159357b28a79a2cfba87bbd3
parent28db0f239f18f3ecfb37ac302529773a1d8ac064 (diff)
r8686@thot: notin | 2006-03-20 19:29:09 +0100
Correction d'un bug dans Coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8661 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--tools/coqdoc/pretty.mll5
1 files changed, 4 insertions, 1 deletions
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 2acb414074..096e64a818 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -404,7 +404,7 @@ and coq = parse
let eol = body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| space+ { char ' '; coq lexbuf }
- | eof
+ | eof
{ () }
| _ { let eol =
if not !gallina then
@@ -567,6 +567,9 @@ and body = parse
| identifier
{ let s = lexeme lexbuf in
ident s (lexeme_start lexbuf); body lexbuf }
+ | token
+ { let s = lexeme lexbuf in
+ symbol s; body lexbuf }
| _ { let c = lexeme_char lexbuf 0 in
char c; body lexbuf }