[PG/Company] Structured outline mode

Using Rocq
1

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.

2

Hi,

This sounds like a feature request to company-coq or PG so would seem more appropriate for their issue trackers, but since some of their maintainers are there anyway, I’ll tag them. @erikmd @Matafou

3

I created an issue in the company-coq repo.