Issues

• Suggest Proof Using handling broken on Rocq master

  ProofGeneral/PG#896 · Filter by author SkySkimmer opened on Oct 30, 2026

• Identifier called "Error" triggers error

  ProofGeneral/PG#886 · Filter by author rudynicolop opened on Oct 12, 2026

• coq-mode fails to start on .v files with byte-compiled PG: (void-function cl-find-if) when cl-lib is not yet loaded

  ProofGeneral/PG#885 · Filter by author amanda4zx opened on Sep 29, 2026

• New 9.2 keywords not colored

  ProofGeneral/PG#877 · Filter by author fblanqui opened on Jul 6, 2026
  1

• CL block names should be symbols not arbitrary sexps

  ProofGeneral/PG#873 · Filter by author monnier opened on Apr 9, 2026

• defadvice is obsolete

  ProofGeneral/PG#872 · Filter by author monnier opened on Apr 9, 2026

• Loading pg-custom breaks PG

  ProofGeneral/PG#871 · Filter by author monnier opened on Apr 9, 2026

• coq-prog-name disregarded and overwritten

  ProofGeneral/PG#869 · Filter by author hendriktews opened on Feb 26, 2026
  3

• Unable to run coqtop/rocq when using opam switches

  ProofGeneral/PG#866 · Filter by author RangHo opened on Jan 30, 2026
  1

• Put autodetected coq version in modeline?

  ProofGeneral/PG#864 · Filter by author SkySkimmer opened on Jan 19, 2026
  4

• wish: have a visual highlighting of the last command (especially if it triggers an error).

  kind: enhancement
  Feature

  ProofGeneral/PG#859 · Filter by author Matafou opened on Jan 4, 2026
  

• empty response for info_auto tactic

  ProofGeneral/PG#851 · Filter by author yaitskov opened on Nov 24, 2025
  1

• Proof General may be forced to run Rocq completely silent for Rocq 9.2

  ProofGeneral/PG#843 · Filter by author hendriktews opened on Sep 1, 2025
  4

• error wrong queuemode in proof-add-to-queue: t instead expected advancing

  ProofGeneral/PG#836 · Filter by author hendriktews opened on Jun 29, 2025

• diffs not shown when Coq is run completely silent

  ProofGeneral/PG#835 · Filter by author Flupp opened on Jun 23, 2025
  2

• Debugging slow proofgeneral issues for Coq

  ProofGeneral/PG#830 · Filter by author vmurali opened on May 14, 2025
  1

• proof tree error when coq-auto-adapt-printing-width is nil

  ProofGeneral/PG#829 · Filter by author hendriktews opened on May 12, 2025

• Is t a permitted value for proof-shell-busy and what does it mean?

  ProofGeneral/PG#828 · Filter by author hendriktews opened on May 12, 2025
  2

• Menu Show Tree yields error

  ProofGeneral/PG#826 · Filter by author hendriktews opened on May 10, 2025

• coq-LocateNotation does not add quotes

  ProofGeneral/PG#825 · Filter by author hendriktews opened on May 10, 2025

• (deprecation) warnings not shown when a tactic fails to apply

  ProofGeneral/PG#824 · Filter by author hoheinzollern opened on Apr 4, 2025
  1

• docker pull limit exceeded in CI

  ProofGeneral/PG#823 · Filter by author hendriktews opened on Apr 3, 2025
  8

• Rocq proofs are not omitted when there are numbered selectors

  ProofGeneral/PG#821 · Filter by author upamanyus opened on Apr 1, 2025
  7

• Recent MR to support rocq binary broke "hacks" that allow changing coq-prog-name

  ProofGeneral/PG#819 · Filter by author gmalecha opened on Apr 1, 2025
  7

• Need help understanding indentation?

  ProofGeneral/PG#818 · Filter by author patrick-nicodemus opened on Mar 31, 2025