Hi,
Company/PG has the command M-x company-coq-occur
(bound to C-c C-,
in my case), which gives an outline of the curent lemmas/definitions/etc. However, it doesn’t follow the coqdoc
structure. I use special comments to structure my script, like
(** * Title *)
(** ** Chapter *)
(** *** Section *)
(** **** etc *)
It would be nice to have an outline like this in PG/Company, like reftex
's TOC (M-x reftex-toc
). This would help navigating in large .v
files.