#418 |
Emacs is not responding after typing `Case "".<newline>`
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#419 |
Print Fully Explicit option gets out of sync after undoing before point where it was changed
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
7:prover-coq
|
#420 |
Another Emacs indentation freeze
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#421 |
proof-shell-exit raises an exception "Buffer foo.v has no process"
|
coquser
|
defect
|
critical
|
PG-Emacs-4.1
|
2:pg-emacs
|
#422 |
Support for entering ellipsis in electric terminator mode
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#423 |
List customisation variables use wrong widget
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#424 |
proof-shell-exit does not follow standard emacs policy with query-exit.
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#426 |
proof-user-options custom group partly broken
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#428 |
subsubsection links not working in PG doc
|
David Aspinall
|
defect
|
critical
|
PG-Emacs-4.2
|
2:pg-emacs
|
#430 |
Make "Set Ltac Debug" work
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#432 |
Add documentation of *trace* buffer to PG Adapting manual
|
David Aspinall
|
task
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#434 |
phox seems completely broken
|
David Aspinall
|
defect
|
critical
|
PG-Emacs-4.3
|
2:pg-emacs
|
#435 |
wrong behaviour of the period
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#436 |
Starting the coq process results in an error
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#437 |
compilation error with LANG=C
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#440 |
User manual link on development page broken
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#441 |
make -C doc magic fails
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#443 |
Retracting, editing, then re-evaluating/proving sometimes results in definitions that do not match the contents of the file
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#444 |
three windows mode at pg start when a warning window
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#446 |
window-live-p error (coq, aquamacs)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#449 |
coq electric terminator conflict
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#450 |
Proof in proof tree
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#451 |
support {} and bullets in prooftree
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#452 |
Some Isabelle options enabled but not active
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#458 |
ProofGeneral 4.2 byte-compilation fails with Emacs 24.2.90
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#461 |
old manuals on website
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#463 |
Warning messages suppress error messages and make PG have incorrect behavior with Coq
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#466 |
parentheses in comments should not affect indentation level of non-comment code
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#467 |
The "Time (tactic)." vernacular command no longer displays timings unless the tactic finishes the proof
|
hendrik
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#470 |
texinfo 5.1 incompatibility
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#471 |
ProofGeneral.jpg missing in ProofGeneral-4.3pre130510.tgz
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#472 |
texi2pdf loads Proofgeneral.pdf as image
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#473 |
Indentation screwed up by "/." (not by "/ .") in, e.g., [Arguments foo /.]
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#474 |
Indentation screwed up in sigT notations ("{ _ : _ & _ }") spanning multiple lines
|
courtieu
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#475 |
[exists] tactic causes improper indentation
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#476 |
[Goal], [Proposition], [Intance], [Fixpoint], [Corollary] do not have indented proof scripts
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#477 |
[Proposition] is not highlighted like [Lemma]
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#478 |
[Proof <body term>.] messes up following indentation
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#479 |
[intros ??.] messes up following indentation
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#482 |
[lazymatch] should be highlighted and indented like [match]
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#484 |
[Existing Instances] should be highlighted like [Existing Instance]
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#485 |
"Time commands" option offsets the cursor when errors are reported
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#486 |
Disable long indention under quantifiers?
|
courtieu
|
defect
|
minor
|
PG-Emacs-4.3
|
3:pg-broker
|
#487 |
Coq syntax highlighting: Proposition
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#489 |
Electric Terminator mode breaks desktop-save-mode
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#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
|
PG-Emacs-4.3
|
2:pg-emacs
|
#494 |
PG incorrectly parses the result of [Fail] in some cases
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#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
|
PG-Emacs-4.3
|
2:pg-emacs
|
#502 |
Latest Makefile change breaks things everywhere except Mac
|
David Aspinall
|
defect
|
blocker
|
PG-Emacs-4.3
|
2:pg-emacs
|
#503 |
Some coq output get lost for query processed just after an error stops the queue.
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#504 |
Minor fix for coq-is-symbol-or-punct and coq-grab-punctuation-left
|
cpitcla
|
enhancement
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#505 |
Fix indentation of lazymatch in Coq
|
cpitcla
|
enhancement
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#512 |
test.coq target doesn't exist
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|