Skip to content

Issues: ProofGeneral/PG

Beta
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

219 Open 330 Closed
219 Open 330 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Menu Show Tree yields error
#826 opened May 10, 2025 by hendriktews
coq-LocateNotation does not add quotes
#825 opened May 10, 2025 by hendriktews
(deprecation) warnings not shown when a tactic fails to apply
#824 opened Apr 4, 2025 by hoheinzollern
1
docker pull limit exceeded in CI
#823 opened Apr 3, 2025 by hendriktews
8
Rocq proofs are not omitted when there are numbered selectors
#821 opened Apr 1, 2025 by upamanyus
7
Recent MR to support rocq binary broke "hacks" that allow changing coq-prog-name
#819 opened Apr 1, 2025 by gmalecha
3
Need help understanding indentation?
#818 opened Mar 31, 2025 by patrick-nicodemus
Delay when first command produces an error
#814 opened Mar 20, 2025 by SkySkimmer
2
Use rocq repl instead of coqtop when available
#811 opened Feb 11, 2025 by SkySkimmer
1
deficiencies when changing processed comments
#809 opened Jan 27, 2025 by hendriktews
1
Print Tables treated as error
#806 opened Jan 16, 2025 by SkySkimmer
2
Subgoal bullet auto completition
#805 opened Jan 6, 2025 by yaitskov
Task: improve/harden the pg-protected-undo function
#803 opened Nov 23, 2024 by erikmd
1
Library compilation failed
#801 opened Nov 21, 2024 by usr345
11
undo does not retract when undoing a comment created by comment-dwim
#800 opened Nov 20, 2024 by hendriktews
16
Compiler warnings: wrong usage of unescaped single quotes
#795 opened Oct 8, 2024 by andreas-roehler
PG gets confused by comment in _CoqProject file that involves "-arg"
#794 opened Oct 3, 2024 by RalfJung
1
Incompatibility with package-quickstart kind: bug kind: fix
#771 opened Jun 8, 2024 by monnier
7
Why retracting before restarting coqtop?
#770 opened Jun 7, 2024 by Matafou
3
Proof General gets into a state where it doesn't know what + is.
#769 opened Jun 5, 2024 by walck
11
UI and kernel out of sync from aborting tactics?
#764 opened Apr 25, 2024 by AndreasLoow
1
different styles of comment
#756 opened Apr 3, 2024 by ElifUskuplu
6
Bug: Frames in hybrid mode automatically revert to vertical mode
#746 opened Mar 16, 2024 by allen-liaoo
2
coq-load-project file should extract META files
#736 opened Feb 12, 2024 by hendriktews
1
void function error
#734 opened Feb 5, 2024 by ZHANGTIANYAO1
ProTip! no:milestone will show everything without a milestone.