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

208 Open 326 Closed
208 Open 326 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

(Some) vok compilation seems to ignore coq-compiler
#797 opened Oct 31, 2024 by LukeXuan
6
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
PG does not position to error of vernacular commands
#790 opened Sep 30, 2024 by hendriktews
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
Indentation issue : "\in" kind: bug part: indentation Problems with indentation feature of PG
#757 opened Apr 4, 2024 by KimayaBedarkar
2
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
test_wholefile.v incompatible with 8.19 kind: bug kind: test
#719 opened Dec 26, 2023 by hendriktews
4
coq-insert-suggested-dependency sometimes inserts unparsable statements
#715 opened Nov 8, 2023 by HazardousPeach
Colors don't work in emacs-nox
#709 opened Oct 9, 2023 by cryslith
1
Automatic indenting for Easycrypt
#702 opened Aug 2, 2023 by Adamw1NCSC
1
Merging the Abella fork of PG
#701 opened Jul 22, 2023 by phikal
11
Scheme ... with is indented improperly
#700 opened Apr 25, 2023 by audreyseo
1
test_wholefile.v incompatible with 8.17
#698 opened Apr 8, 2023 by hendriktews
@erikmd @CyrilAnac
1
whitelist for admissible commands inside proofs kind: enhancement
#689 opened Feb 26, 2023 by hendriktews
17
Tons of warnings when using certain PG features
#686 opened Jan 31, 2023 by RalfJung
12
Broken link in Ch. 11 of User's Manual kind: documentation
#678 opened Nov 26, 2022 by rebcabin
Update https://proofgeneral.github.io/ kind: documentation
#673 opened Oct 4, 2022 by monnier
2
Feedback from Coq Community Survey 2022.
#671 opened Sep 30, 2022 by Zimmi48
1
ProTip! Adding no:label will show everything without a label.