Erik Martin-Dorel

deps bug (`coq-serapi` incompatible with newest `cmdliner`, making some Docker-Coq builds fail) + question

6

Hi @ejgallego, FYI after the bump of opam to 2.1.2 in `coqorg/base` (coq-community/docker-base#17), I rebuilt all `coqorg/coq` images ([pipeline](https://gitlab.com/coq-community/docker-coq/-/pipelines/507529655)) but some jobs failed: https://gitlab.com/coq-community/docker-coq/-/jobs/2284076471 https://gitlab.com/coq-community/docker-coq/-/jobs/2284076472 with the same error: ```bash...

feat(docutils): Use `section_self_link` (needs html5 + CSS update)

12

I recently noticed that despite the availability of this new feature in docutils: https://sourceforge.net/p/docutils/feature-requests/28/ (which BTW can only be enabled **in HTML5**), the feature requested in cpitclaudel/alectryon#19 was not yet...

Why does code following a .. code-block end up nested into it?

9

Hi @cpitclaudel, I'm not sure but I believe I found a small bug when processing `alectryon.py --frontend coq+rst --backend webpage foo.v` on this `foo.v` file: ```coq Check nat. (* .unfold...

Improve (company-coq-occur) to cope with non-one-liner statements?

2

Dear @cpitclaudel, @pPomCo and I like the `(company-coq-occur)` function very much (bound to `C-c C-,`) but it often happens that definitions and lemmas are not one-liners… so that we end...

When the DIffs feature (recently added in PG by @jfehrle) is enabled (menu `Coq > Diffs > "on"`), the extraction lemma C-c C-a C-x doesn't work out-of-the-box. MWE: ``` Require...

Loading company-coq prevents PG context menu to appear

2

*[Follow-up of ]* Using current PG master and company-coq from MELPA, a right-click on a Coq phrase doesn't make the standard PG context menu to appear (for the expected feature,...

When enabling the "automatic Show Proof Diffs feature" (#487), the output of regular commands such as `Check nat.` etc. is not shown anymore. Here is another unexpected side effect: ```coq...

The [ci](https://github.com/ProofGeneral/PG/tree/master/ci) folder has been significantly extended by @hendriktews (and organized in several subfolders) when adding new tests, so the tests I had initially added could be structured in a...

As pointed out in PR https://github.com/ProofGeneral/PG/pull/501, it would be nice to add at least one integration test for EasyCrypt in the GitHub-actions based CI. For the record, the two main...

TODO: * Add `info` documentation for #490 * Add summary in `CHANGES`