diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-04 13:05:58 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-04 13:05:58 +0000 |
| commit | 79fba16cf02b83ac2b4866e582dd4481314770b4 (patch) | |
| tree | a6f268fe0edc8811bc8222c46503aa828da885eb /tools | |
| parent | 75862b96afd73704bc56f52ef2375d128ad53150 (diff) | |
Correction bug #1204 + maj CHANGES
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9204 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/index.mll | 1 | ||||
| -rw-r--r-- | tools/coqdoc/pretty.mll | 23 |
2 files changed, 14 insertions, 10 deletions
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index 5278945ef..4e5404447 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -364,6 +364,7 @@ and end_ident = parse and module_ident = parse | space+ { module_ident lexbuf } + | '"' { string lexbuf; module_ident lexbuf } | ident space* ":=" { () } | ident diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index 2de6838ea..869df4eef 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -398,19 +398,22 @@ and coq = parse { () } | gallina_kw_to_hide { let s = lexeme lexbuf in - if !light && section_or_end s then begin - let eol = skip_to_dot lexbuf in - if eol then coq_bol lexbuf else coq lexbuf - end else begin - ident s (lexeme_start lexbuf); - let eol=body lexbuf in - if eol then coq_bol lexbuf else coq lexbuf - end } + if !light && section_or_end s then + begin + let eol = skip_to_dot lexbuf in + if eol then coq_bol lexbuf else coq lexbuf + end + else + begin + ident s (lexeme_start lexbuf); + let eol=body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf + end } | gallina_kw { let s = lexeme lexbuf in ident s (lexeme_start lexbuf); - let eol = body lexbuf in - if eol then coq_bol lexbuf else coq lexbuf } + let eol = body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } | space+ { char ' '; coq lexbuf } | eof { () } |