PG
PG copied to clipboard
ProofGeneral
This repo is the new home of Proof General
I had refactored PG's behavior w.r.t. `C-_` a long time ago (which was fairly broken before my patches) There is a **limitation** of the current algorithm of "pg-protected-undo": 1. one...
With this change the TAGS file can also jump to class names, constructors and projections.
Preserves buffer-local environment e.g. `exec-path` so that `coq-detect-rocq-cli` executes the Rocq executable in the same environment as it is executed in other parts of PG. Also a slightly simpler implementation....
Hi. PG gets frozen with the following file when we reach the line 3: ``` Axiom Ninterval: nat -> nat -> Prop. Notation "[ n '....' m ]" := (Ninterval...
The first commit is just a reformatting commit (to make the code easier to read). The second commit is the significant one, and this is its commit message: **Snapshot match...
Hi, `info_auto` tactic runs `auto` tactic with logging but the `*response*` buffer is empty. coqtop output: > (* info auto: *) > intro. > intro. > intro. > intro. >...
~~~coq Fail Check 0 : 0. ~~~ should say "The command has indeed failed with message: ..." in `*response*` but says nothing (the message is still visible in `*coqù*` though)
Disable Set Silent for Rocq >= 9.2, which does not print any goals any more. See also PR 21038 for Rocq. Fixes #842 #849 #843
Since PR #762 has been merged, Proof General sets option `Silent` in coq/rocq and never clears it, such that the background coq/rocq runs completely silent. This fixes many problems with...
The warning looks like this (from the `*Warnings*` buffer): ``` ⛔ Warning (files): Missing ‘lexical-binding’ cookie in "~/.emacs.d/.cache/elpaca/builds/proof-general/generic/proof-autoloads.el". You can add one with ‘M-x elisp-enable-lexical-binding RET’. See ‘(elisp)Selecting Lisp Dialect’...
