Is this a bug or a misuse of coqdoc ?
"<<<" inside a comment is not rendered and causes a change of font in the generated html page.
Example: when process by coqdoc 8.11, the following comment
(* Alternative notation displays can be defined by : *) (* 1. declaring a new opaque definition of type unit. Using the idiom *) (* `Lemma my_display : unit. Proof. exact: tt. Qed.` *) (* 2. using this symbol to tag canonical porderType structures using *) (* `Canonical my_porderType := POrderType my_display my_type my_mixin`, *) (* 3. declaring notations for the main operations of this library, by *) (* setting the first argument of the definition to the display, e.g. *) (* `Notation my_syndef_le x y := @Order.le my_display _ x y.` or *) (* `Notation "x <<< y" := @Order.lt my_display _ x y (at level ...).` *) (* Non overloaded notations will default to the default display. *) (* *) (* One may use displays either for convenience or to disambiguate between *) (* different structures defined on "copies" of a type (as explained below.) *) (* We provide the following "copies" of types, *) (* the first one is a *documented example* *) (* natdvd := nat *) (* == a "copy" of nat which is canonically ordered using *) (* divisibility predicate dvdn. *) (* Notation %|, %<|, gcd, lcm are used instead of *) (* <=, <, meet and join. *)
generates the following html page:
<< is documented here
Last updated: Feb 01 2023 at 11:04 UTC