PG
PG copied to clipboard
ProofGeneral
This repo is the new home of Proof General
MELPA dist seems to fail on my machine. In particular, paths seem badly configured. For instance, all files in `coq/` fail to compile if they have local dependencies, e.g. `coq-syntax.el`....
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...
Hi @Matafou Thanks for your work on the new indentation engine! Here are a few things that could be improved. The following samples are indented how I would expect them;...
**Environment:** Mac, Emacs 27.2, Coq 8.13.2, PG 20220310.2253; also VS Code 1.65.2, VSCoq 0.3.6; Coq_Platform_2021.09.0; and the online Scratchpad jsCoq 0.15.0, Coq 8.15.0. **Steps to reproduce:** 1. Put this code...
```coq Notation "a -:" := (id a) (at level 9, format "a -:"). Lemma test(foo: nat) : foo-: = foo. ``` displays ``` foo : nat ============================ foo-: = foo...
Hi, I wonder what is the expected behavior when proof-multiple-frames-enable is set to t. I'm using PG on macOS and spacemacs. I was expecting that at least the `*goals*` buffer...
I tried the following code: ``` Goal True ∧ True. split. { Time auto. ``` When I run this in coqtop, it prints something like ``` Finished transaction in 0....
See checks in PR #632. The error seems to be independent of Emacs, in PR #626 the test fails with Coq 8.14 with all tested emacs versions. @erikmd I believe...
The old web pages at inf.ed.ac.uk are likely to be fully decommissioned soon. I've hastily removed most of the main links from documentation files (in the master branch only). Some...
