Skip to content

/ 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.

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

148 Open 246 Closed
148 Open 246 Closed
Author
Filter by author
Label
Filter by label
Use alt + click/return to exclude labels.
Projects
Filter by project
Milestones
Filter by milestone
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀
ProofGeneral being broken in melpa-stable is confusing kind: infrastructure kind: question
#509 opened Aug 18, 2020 by samontea
3
Defining coq-mode-abbrev-table as '() still keeps abbrevs
#508 opened Jul 29, 2020 by jpprime
Add some EasyCrypt integration test to the CI? help wanted kind: infrastructure kind: test
#505 opened Jun 20, 2020 by erikmd
Output of "Time" is hidden when this is the last goal in a "{...}"
#502 opened Jun 19, 2020 by RalfJung
2
ProofGeneral does not understand vos files
#500 opened Jun 15, 2020 by RalfJung
19
Add documentation for #490 - Improve PG support of Show Proof Diffs kind: documentation
#497 opened May 29, 2020 by erikmd
@erikmd
macro to expand "by rewrite A B C ... ." kind: feature
#494 opened May 26, 2020 by chdoc
21
Per-project switch selection kind: feature
#481 opened Apr 16, 2020 by Lysxia
2
Dune support
#477 opened Apr 2, 2020 by ejgallego
26
Can't compile from melpa
#471 opened Mar 13, 2020 by Boarders
10
Indentation issue: intros with `?`
#466 opened Mar 5, 2020 by joonwonc
2
Goals window not refreshing after `Proof.`
#461 opened Feb 18, 2020 by samuelgruetter
2
Local Unicode Tokens?
#460 opened Feb 15, 2020 by kindaro
Indentation issue: ssreflect's "have :="
#459 opened Feb 14, 2020 by Ptival
Every command to Coq also sends "Show." and gets error "This command requires an open proof."
#458 opened Feb 13, 2020 by jeapostrophe
5
PG "processes" bogus tactics
#457 opened Feb 13, 2020 by Ptival
1
No syntax highlighting at first lauch
#456 opened Feb 13, 2020 by ckeller
5
Indentation issue: "forall"
#454 opened Jan 30, 2020 by RalfJung
10
Indentation issue: "by"
#453 opened Jan 30, 2020 by RalfJung
1
Infinite Loop when using "-noinit", with solutions inside.
#449 opened Dec 16, 2019 by scinart
imenu support
#448 opened Dec 14, 2019 by vzaliva
1
Indent proof after colon
#442 opened Sep 29, 2019 by liyishuai
1
Misc indentatiosn requests
#441 opened Sep 26, 2019 by cpitclaudel
1
Coq PG doesn't recognize the new quotation mechanism of coq/coq#9733
#437 opened Aug 8, 2019 by pi8027
4
Extremely long lines stall the processing
#436 opened Jul 31, 2019 by Ptival
2
ProTip! Exclude everything labeled bug with -label:bug.
You can’t perform that action at this time.