Issues

• 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

• Inconsistent indentation between Inductive and Variant

  ProofGeneral/PG#882 · Filter by author jeremyThibault opened on Aug 24, 2026

• Can't go back in proofs, or display is wrong with Rocq 9.2

  ProofGeneral/PG#881 · Filter by author tperami opened on Aug 12, 2026
  3

• New 9.2 keywords not colored

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

• generic/proof-autoloads causes emacs startup error trying to load ../lib/holes, which has been removed

  ProofGeneral/PG#876 · Filter by author cxandru opened on May 26, 2026
  8

• Rocq 9.2 + auto compilation = spurious recompilations

  kind: bugkind: regressionneeds: fixingpart: coq-compile
  Bug

  ProofGeneral/PG#875 · Filter by author Matafou opened on Apr 17, 2026
  4

• 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

• "No more goals" hides other message (in completely-silent mode)

  ProofGeneral/PG#870 · Filter by author SkySkimmer opened on Apr 3, 2026
  6

• 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

• Disappearance of all infomsg

  ProofGeneral/PG#842 · Filter by author proux01 opened on Aug 19, 2025
  14

• 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
  1

• 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