Erik Martin-Dorel

Thanks @phikal for opening this issue! @chaudhuri > If anything, I think the onus is on Abella to provide a suitable PR for PG if indeed Abella thinks it is...

Hi @chaudhuri @phikal, as said earlier, a new PR (that could take inspiration from https://github.com/ProofGeneral/PG/pull/636) adding Abella support in PG would be welcome. We'd give you feedback within one such...

Hi @hendriktews, good catch; but IINM, the `test_wholefile.v` was intended to test PG capabilities on a realistic Coq example. It appears the test file rusted, but maybe a better solution...

> Seeing it now failing again because of a deprecated feature after nobody had reacted to https://github.com/ProofGeneral/PG/issues/698 Yes, sorry 😅 > and seeing that the code is far below my...

Hi @monnier ! Thanks for your comment. FYI the source code of the webpage you are talking about ( https://proofgeneral.github.io/ ) is hosted here: https://github.com/ProofGeneral/proofgeneral.github.io/blob/master/index.md Feel free to open a...

Note that this is Markdown + Jekyll syntax, implying e.g. that code between: ``` {% comment %} {% endcomment %} ``` is ignored.

Thanks a lot @Zimmi48 for summarizing all this! Very useful feedback

@hendriktews I didn't skim the Coq refman right now, but I'd suggest to check the list of Coq commands recognized by PG's C-c C-v as state-preserving. Maybe there's a strong...

Yes I know. What I meant is that: thanks to this command, PG already maintains a list of all Coq commands that are state-preserving. Certainly not exhaustive w.r.t. the whitelist...

Hi @Matafou > I see a few that are state changing (Opaque etc). Don't even know why they are here. That's just a small bug! * I opened PR https://github.com/ProofGeneral/PG/pull/692...