Search results

New 9.2 keywords not colored

Status: Open.

#877 In ProofGeneral/PG;

· fblanqui opened on Jul 6, 2026

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

Status: Open.

#876 In ProofGeneral/PG;

· cxandru opened on May 26, 2026

Rocq 9.2 + auto compilation = spurious recompilations

kind: bug

kind: regression

needs: fixing

part: coq-compile

Status: Open.

Bug

#875 In ProofGeneral/PG;

· Matafou opened on Apr 17, 2026

CL block names should be symbols not arbitrary sexps

Status: Open.

#873 In ProofGeneral/PG;

· monnier opened on Apr 9, 2026

defadvice is obsolete

Status: Open.

#872 In ProofGeneral/PG;

· monnier opened on Apr 9, 2026

Loading pg-custom breaks PG

Status: Open.

#871 In ProofGeneral/PG;

· monnier opened on Apr 9, 2026

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

Status: Open.

#870 In ProofGeneral/PG;

· SkySkimmer opened on Apr 3, 2026

coq-prog-name disregarded and overwritten

Status: Open.

#869 In ProofGeneral/PG;

· hendriktews opened on Feb 26, 2026

Unable to run coqtop/rocq when using opam switches

Status: Open.

#866 In ProofGeneral/PG;

· RangHo opened on Jan 30, 2026

Put autodetected coq version in modeline?

Status: Open.

#864 In ProofGeneral/PG;

· SkySkimmer opened on Jan 19, 2026

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

kind: enhancement

Status: Open.

Feature

#859 In ProofGeneral/PG;

· Matafou opened on Jan 4, 2026

empty response for info_auto tactic

Status: Open.

#851 In ProofGeneral/PG;

· yaitskov opened on Nov 24, 2025