aboutsummaryrefslogtreecommitdiff
path: root/test-suite/coqdoc/bug5700.v
AgeCommit message (Collapse)Author
2020-11-14Addressing #13304: how to verbatim an expression mentioning >>.Hugo Herbelin
We clarify that there are two kinds of verbatim: inline and block. We add a test testing verbatim and others. Co-authored-by: Xia Li-yao <Lysxia@users.noreply.github.com>
2017-08-29coqdoc: Support comments in verbatim outputTej Chajed
Fixes BZ#5700