diff options
| -rw-r--r-- | tools/coqdoc/output.ml | 4 | ||||
| -rw-r--r-- | tools/coqdoc/pretty.mll | 11 |
2 files changed, 2 insertions, 13 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index cbb435f4aa..1fa8b892c2 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -363,8 +363,8 @@ module Html = struct let latex_char _ = () let latex_string _ = () - let html_char = char - let html_string = raw_ident + let html_char = output_char + let html_string = output_string let start_latex_math () = () let stop_latex_math () = () diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index 7f5f782f07..02a0a78487 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -400,10 +400,6 @@ and doc = parse { escaped_html lexbuf; doc lexbuf } | "##" { char '#'; doc lexbuf } - | "^" - { escaped lexbuf; doc lexbuf } - | "^^" - { char '^'; doc lexbuf } | eof { false } | _ @@ -430,13 +426,6 @@ and escaped_html = parse | eof { () } | _ { html_char (lexeme_char lexbuf 0); escaped_html lexbuf } -and escaped = parse - | "^" { () } - | "^^" - { hard_verbatim_char '^'; escaped lexbuf } - | eof { () } - | _ { hard_verbatim_char (lexeme_char lexbuf 0); escaped lexbuf } - and verbatim = parse | "\n>>" { verbatim_char '\n'; stop_verbatim () } | eof { stop_verbatim () } |