diff options
| -rw-r--r-- | tools/coqdoc/pretty.mll | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index 1a2c5d866d..e0d2a3c99c 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -638,6 +638,9 @@ and notation_bol = parse and notation = parse | nl { line_break(); notation_bol lexbuf } | '"' { char '"'; false } + | token + { let s = lexeme lexbuf in + symbol s; notation lexbuf } | _ { let c = lexeme_char lexbuf 0 in char c; notation lexbuf } |