We have a comment like this in our code:
(** The general approach we use for all these complex notations: an outer '[hv' to switch bwteen "horizontal mode" where it all fits on one line, and "vertical mode" where each '/' becomes a line break. Then, as appropriate, nested boxes ('['...']') for things like preconditions and postconditions such that they are maximally horizontal and suitably indented inside the parentheses that surround them. *)
This makes coqdoc print a warning, since it tries to interpret the
'[hv as the beginning of inline code. Is there a way to escape the bracket so coqdoc doesnt get confused and we dont have warnings in our build?
IIRC you can place square brackets inside other square brackets at will. So
['[hv'] should work, although it will typeset it as code.
@Ralf Jung, you can also pass the
--plain-comments to coqdoc
that would affect all comments though, not just this one
>> delimits code blocks)
Last updated: Jan 31 2023 at 13:02 UTC