#364 |
Unify proof-query-identifier and pg-identifier-near-point-query (cleanup)
|
accepted
|
David Aspinall
|
task
|
trivial
|
2:pg-emacs
|
#208 |
Generalise Coq's modeline subgoal counter for other provers
|
accepted
|
David Aspinall
|
enhancement
|
minor
|
2:pg-emacs
|
#336 |
Toolbar images on Mac Emacsen are super-ugly
|
reopened
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
#361 |
Generic adjustment of prover's pretty-printing width
|
accepted
|
David Aspinall
|
task
|
minor
|
2:pg-emacs
|
#385 |
Isabelle theorem dependencies display broken
|
accepted
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
#401 |
Parser cache does not respect fly-past-comments
|
accepted
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
#457 |
Remove/invoke proof-shell-pre-interrupt-hook
|
new
|
David Aspinall
|
task
|
minor
|
2:pg-emacs
|
#464 |
proof script not displayed after startup
|
new
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
#465 |
proof script not displayed after startup
|
new
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
#480 |
[match]es sometimes screw up indentation
|
new
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
#481 |
proof-set-value does not handle errors in :eval forms of defpacustom
|
new
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
#483 |
ltac: and constr: should not affect indentation
|
new
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
#490 |
Bad parsing of .}
|
new
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
#496 |
Aquamacs point moving
|
new
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
#497 |
coq auto-compile and spaces in directory names lead to failure
|
new
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
#499 |
delays between coq messages can cause PG to duplicate some
|
new
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
#501 |
wrongly embedded pathname in ProofGeneral-4.3pre150202
|
new
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
#506 |
Please add Proof IDE support to emacs PG
|
new
|
David Aspinall
|
enhancement
|
minor
|
2:pg-emacs
|
#507 |
PG for Coq does not interpret quotes within comments like Coq does
|
new
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
#508 |
The option -emacs-U is depracated Proof General should use -emacs instead.
|
new
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
#509 |
isar/isar-unicode-tokens.el:687:1:Error: the function `isar-markup-ml' is not known to be defined.
|
new
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
#510 |
coq-time-commands hangs on bullets with Coq-8.5
|
new
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
#514 |
Emacs org-mode integration
|
new
|
David Aspinall
|
enhancement
|
minor
|
2:pg-emacs
|
#169 |
Complete buffer history enhancement
|
assigned
|
David Aspinall
|
enhancement
|
major
|
2:pg-emacs
|
#273 |
next-error functions: document and streamline
|
accepted
|
David Aspinall
|
enhancement
|
major
|
2:pg-emacs
|
#276 |
Unicode tokens: resolve font-lock issues, optimise
|
accepted
|
David Aspinall
|
task
|
major
|
2:pg-emacs
|
#351 |
Show/hide of proofs in Coq can hide too much
|
accepted
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
#367 |
Fix web pages and update screenshots
|
accepted
|
David Aspinall
|
task
|
major
|
2:pg-emacs
|
#377 |
Electric-terminator mode next line movement changed
|
reopened
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
#425 |
Consider simplifying span amalgamation to match prover undo behaviour
|
accepted
|
David Aspinall
|
task
|
major
|
2:pg-emacs
|
#429 |
Coq should support *trace* buffer for idtac output
|
reopened
|
David Aspinall
|
enhancement
|
major
|
2:pg-emacs
|
#448 |
Repair autotest load sequence so works in compiled and interpreted code
|
accepted
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
#454 |
coq mode: compile before import fails when no .v file
|
assigned
|
hendrik
|
enhancement
|
major
|
2:pg-emacs
|
#456 |
initialization failure with defpacustom :eval
|
new
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
#498 |
coq-compile-before-require should allow non-source installations
|
new
|
David Aspinall
|
defect
|
major
|
7:prover-coq
|