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:

image.png

Actually `<<`

is documented here

Last updated: Feb 01 2023 at 11:04 UTC