summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/coq2html.mll4
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/coq2html.mll b/doc/coq2html.mll
index da2e602..dd7d3a9 100644
--- a/doc/coq2html.mll
+++ b/doc/coq2html.mll
@@ -372,6 +372,10 @@ and doc = parse
{ character '\n'; doc_bol lexbuf }
| "["
{ start_bracket(); bracket lexbuf; end_bracket(); doc lexbuf }
+ | "$" [^ '\n' '$']* "$"
+ { doc lexbuf }
+ | "#" ([^ '\n' '#']* as html) "#"
+ { output_string !oc html; doc lexbuf }
| eof
{ () }
| _ as c