Pierre Courtieu
Pierre Courtieu
Hi there! I think a few hings can be updated in the tutorial, for a better experience. 1. The current version of the tutorial starts with a call to `SearchAbout`,...
Hi When a new tactic appear, it gets surreounded byt tags when in diff mode. It makes company-coq not recognize its name and hence it is not proposed as completion....
Hi there, when completing a hypothesis name and scrolling in the completion popup menu, it would be nice to have the selected hypothesis be highlighted in the goals buffer. So...
Hi, When writing tactics one often needs to write hyps names. company-coq should propose that. If possible when inside a tactic hypothesis names should even be proposed first. I can...
Hi. when I try the instruction for debian installation I get a warning and an error. The warnig is because the trust mechanism has changed a bit in debian. The...
I.e. avoid calling `proof-layout-windows` when not absolutely necessary. In particular when switching the scripting buffer (which restarts the coq process) we should avoid destroying the windows sizing and splitting the...
Among other things, PG coq can builds tons of abbrevs from `coq-syntax.el` databases (which I should update by the way). This abbrevs can optionally make use of "holes" which provide...
_CoqProject file has a bash-like comment syntax. `#` starts a comment until the end of the line. But if PG find a _CoqPrpjet file containing, e.g. ``` # -R ....
This is in no way a real pull request, just experiments to understand how we could insert a "Show" command after an error occured. It comes from a discussion with...
Tentative fix for #18332. If the patch is accepted I will add a test in the bench too.