Better support for coqdoc

[annenkov]

It seems like not all coqdoc comments are handled currently. I run into the following issues:

• coqdoc inside definitions renders as comments (** ... *)
• hiding with (* begin hide *) ... (* end hide *) doesn't work.

Here is an example

From Coq Require Import List.

(** * Some functions on lists *)

(** My definition of the [map] function *)

Fixpoint my_map {A B} (f : A -> B) (xs : list A) :=
  match xs with
(** coqdoc inside the definition *)
  | nil => nil
(** more coqdoc *)
  | cons x xs => cons (f x) (my_map f xs)
  end.

(* begin hide *)

Definition should_be_hidden : nat := 0.

(* end hide *)

Alectryon command

alectryon AlectrionCoqdoc.v --frontend coqdoc --backend webpage

Alectryon output

Coq version

The Coq Proof Assistant, version 8.11.2 (November 2021)
compiled on Nov 17 2021 10:04:59 with OCaml 4.08.1

[cpitclaudel]

That's right; the coqdoc frontend was mostly intended as a demonstration, and I haven't worked that much on it. In the long run the hope was the documents would be migrated away from Coqdoc, but I'd welcome help in making support for it better in the meantime.