PG
PG copied to clipboard
ProofGeneral
This repo is the new home of Proof General
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...
Consider this Coq file: ``` Goal True /\ True. Proof. split. { Time tauto. ``` After stepping over the last command, I would expect to see the Coq output that...
A commonly used idiom in the mathematical components library (and many libraries building on top of mathcomp) is to use somthing like `by rewrite A !B /= C D //...
TODO: * Add `info` documentation for #490 * Add summary in `CHANGES`
This is my first partial take on issue #188 and Pierre's example in PR #429 This PR reliably inserts a show command after an error. The following points still need...
Right now when I switch between projects using different Coq versions I have to remember to first do an `opam switch`. Can we tell PG which switch to use on...
With PG-4.4.1~pre at 73792323172e289b531afc086d3f97323b28ecb6 with Coq-8.8 at 37d464bf9c36a8f52b42a509a31739e8afb96f1d, I’m trying to `Require` (with compile-before-require enabled; when this option is disabled, everything works fine) the loader for the toy plug-in at...
PG/xml was not putting a newline at the end of the \*goals\* buffer when there was a single goal. This confused the regexp search in `coq-goals--show-first-goal`. Fixes #233 (I think).
Emacs Mac port supports high-resolution (2x) image display for Retina displays. One way to do that is just to add a file [email protected] in parallel with existing NAME.EXT (no need...
When trying to compile from melpa I get many errors of the form: ``` Error: Wrong type argument: keymapp, nil ``` Any ideas on how I can fix this or...
