#4 |
Use stixfonts once they become available
|
David Aspinall
|
enhancement
|
major
|
1:pg-eclipse
|
fixed
|
#67 |
Move to Java 6...
|
David Aspinall
|
task
|
minor
|
1:pg-eclipse
|
fixed
|
#381 |
Report Emacs bug/issue: slow process filter behaviour on non-Linux platforms
|
David Aspinall
|
task
|
minor
|
2:pg-emacs
|
wontfix
|
#419 |
Print Fully Explicit option gets out of sync after undoing before point where it was changed
|
David Aspinall
|
defect
|
minor
|
7:prover-coq
|
fixed
|
#434 |
phox seems completely broken
|
David Aspinall
|
defect
|
critical
|
2:pg-emacs
|
fixed
|
#442 |
Emacs 24 and long inputs
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
duplicate
|
#446 |
window-live-p error (coq, aquamacs)
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#451 |
support {} and bullets in prooftree
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#452 |
Some Isabelle options enabled but not active
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#455 |
Emacs trunk BZR sometimes hangs when using auto fill mode with PG Coq
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
upstream
|
#458 |
ProofGeneral 4.2 byte-compilation fails with Emacs 24.2.90
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#459 |
Can not split the window vertically
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
wontfix
|
#460 |
proof general hanging on Coq Definition in file generated by Why3
|
hendrik
|
defect
|
major
|
2:pg-emacs
|
worksforme
|
#461 |
old manuals on website
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#463 |
Warning messages suppress error messages and make PG have incorrect behavior with Coq
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#466 |
parentheses in comments should not affect indentation level of non-comment code
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#467 |
The "Time (tactic)." vernacular command no longer displays timings unless the tactic finishes the proof
|
hendrik
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#468 |
Some notations with periods make PG hang
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
wontfix
|
#469 |
coqgeneral 4.3pre130327 does not compile with Emacs 24.3
|
David Aspinall
|
defect
|
blocker
|
2:pg-emacs
|
duplicate
|
#470 |
texinfo 5.1 incompatibility
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#471 |
ProofGeneral.jpg missing in ProofGeneral-4.3pre130510.tgz
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#472 |
texi2pdf loads Proofgeneral.pdf as image
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#473 |
Indentation screwed up by "/." (not by "/ .") in, e.g., [Arguments foo /.]
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#474 |
Indentation screwed up in sigT notations ("{ _ : _ & _ }") spanning multiple lines
|
courtieu
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#475 |
[exists] tactic causes improper indentation
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#476 |
[Goal], [Proposition], [Intance], [Fixpoint], [Corollary] do not have indented proof scripts
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#477 |
[Proposition] is not highlighted like [Lemma]
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#478 |
[Proof <body term>.] messes up following indentation
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#479 |
[intros ??.] messes up following indentation
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#482 |
[lazymatch] should be highlighted and indented like [match]
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#484 |
[Existing Instances] should be highlighted like [Existing Instance]
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#485 |
"Time commands" option offsets the cursor when errors are reported
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#486 |
Disable long indention under quantifiers?
|
courtieu
|
defect
|
minor
|
3:pg-broker
|
fixed
|
#487 |
Coq syntax highlighting: Proposition
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#489 |
Electric Terminator mode breaks desktop-save-mode
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#491 |
Print Implicit not available as emacs command
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
wontfix
|
#492 |
Proof General: script management confused, couldn't find goal span for save. when evaluating past the bottom of a module that contains a theorem with the same name as the module
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#493 |
ProofGeneral stalls/loops on ...
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
wontfix
|
#494 |
PG incorrectly parses the result of [Fail] in some cases
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|
#495 |
Goals buffer aggressively cleared with Coq pre-8.5
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
invalid
|
#500 |
Build fails, due to “'isar-markup-ml' is not known to be defined.” (PG 4.2, Mac OS 10.10.2, Aquamacs 3.2)
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#502 |
Latest Makefile change breaks things everywhere except Mac
|
David Aspinall
|
defect
|
blocker
|
2:pg-emacs
|
fixed
|
#503 |
Some coq output get lost for query processed just after an error stops the queue.
|
David Aspinall
|
defect
|
minor
|
2:pg-emacs
|
fixed
|
#504 |
Minor fix for coq-is-symbol-or-punct and coq-grab-punctuation-left
|
cpitcla
|
enhancement
|
minor
|
2:pg-emacs
|
fixed
|
#505 |
Fix indentation of lazymatch in Coq
|
cpitcla
|
enhancement
|
minor
|
2:pg-emacs
|
fixed
|
#512 |
test.coq target doesn't exist
|
David Aspinall
|
defect
|
major
|
2:pg-emacs
|
fixed
|