Skip to content

Issues: ProofGeneral/PG

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

Clear current search query, filters, and sorts
205 Open 324 Closed
205 Open 324 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

Feedback from Coq Community Survey 2022.
#671 opened Sep 30, 2022 by Zimmi48
1 🎉 1
Free variable smie--parent
#74 opened May 10, 2016 by psteckler
3
3 frames mode - get frames to appear at specific positions with specific sizes
#13 opened Nov 23, 2015 by jonleivent
4
"Setting" menu should we pre-fill string options for all provers
#17 opened Dec 9, 2015 by Matafou
5
ProofGeneral (sometimes?) does not build with Emacs 24.3.1 on Windows
#34 opened Jan 17, 2016 by JasonGross
2
Do we support narrowing?
#35 opened Jan 17, 2016 by cpitclaudel
2
ProofGeneral incorrectly parses unterminated strings in comments in Coq
#37 opened Jan 20, 2016 by JasonGross
24
"Use project file" option does not work
#45 opened Feb 4, 2016 by vzaliva
4
Support ssreflect-style indentation
#51 opened Feb 15, 2016 by ejgallego
10
Edit Abbrevs broken?
#52 opened Feb 16, 2016 by SimonBoulier
2
Electric terminator and newlines
#53 opened Feb 16, 2016 by OndrejSlamecka
5
Buffer coq-compile-response sometimes takes over the whole window resolved: duplicate
#54 opened Feb 17, 2016 by RalfJung
19
Statement splitting incorrect in the presence of some notation help wanted kind: enhancement resolved: wontfix
#58 opened Feb 23, 2016 by RalfJung
9
Cleaning up whitespace shouldn't require rewinding
#4 opened Oct 8, 2015 by cpitclaudel
8
proof-prog-name-ask interacts poorly with tab-completion (especially on Windows)
#86 opened Jul 3, 2016 by JasonGross
4
some idtac output printed multiple times
#94 opened Jul 20, 2016 by jonleivent
1
coq-compile-before-require issue with Coq's command Add LoadPath
#96 opened Aug 1, 2016 by jonleivent
21
coq-end-Section should handle Modules and Module Types
#100 opened Aug 11, 2016 by tchajed
Processing multiple commands terminated with a comment doesn't update proof state
#102 opened Aug 17, 2016 by tchajed
2
Proof state not refreshed after Admitted
#103 opened Aug 17, 2016 by tchajed
3
File mode specification error: (void-variable coq-cmd-force-next-proof-kept)
#775 opened Jun 19, 2024 by DaKnig
14
Multi-line comments formatting
#105 opened Aug 26, 2016 by vzaliva
6
Match does not understand matching on multiple values
#108 opened Sep 9, 2016 by vzaliva
3
Incompatible with company-coq pg: async Related to (unmaintained) async PG with asynchronous Coq proofs
#262 opened Sep 19, 2016 by proofbot
6
Combined Scheme should be highlighted
#73 opened May 8, 2016 by JasonGross
10
ProTip! no:milestone will show everything without a milestone.