#386 |
Coq goals counter not reset on backtracking out of proof
|
courtieu
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#387 |
Preferences lost when prover restarted
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#395 |
proof-segment-up-to-using-cache broken since Oct 11 20:07:17 2010 +0200
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#397 |
Coq PG: changing scripting buffer and automatically restarting misses first command
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#398 |
Compilation failure with mmm and Emacs development version
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#400 |
assert newly added text in ancestor fails
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#403 |
comment-dwim and kill-rectangle in the locked region
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#404 |
Coq parse error with undelimited comment
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#410 |
coq parsing broken since Jun 04 20:12:40
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#412 |
coq parsing broken since Jun 04 20:12:40 (II)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#416 |
Emacs indentation can go into an infinite loop
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#417 |
Website states wrong minimal emacs version
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
6:web-and-docs
|
#418 |
Emacs is not responding after typing `Case "".<newline>`
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#420 |
Another Emacs indentation freeze
|
David Aspinall
|
defect
|
major
|
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
|
#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
|
#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
|
#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
|
#494 |
PG incorrectly parses the result of [Fail] in some cases
|
David Aspinall
|
defect
|
major
|
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
|
#83 |
Fix script parsing to produce reliable and speedy <parseresult> outputs
|
David Aspinall
|
defect
|
critical
|
|
4:prover-isabelle
|
#139 |
Prover not started when run from Product
|
Graham Dutton
|
defect
|
critical
|
|
1:pg-eclipse
|
#421 |
proof-shell-exit raises an exception "Buffer foo.v has no process"
|
coquser
|
defect
|
critical
|
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
|
#434 |
phox seems completely broken
|
David Aspinall
|
defect
|
critical
|
PG-Emacs-4.3
|
2:pg-emacs
|
#24 |
Replace current undo management with document-based undo mechanism
|
David Aspinall
|
defect
|
blocker
|
|
1:pg-eclipse
|
#84 |
Remove double-quoted XML output from term display
|
David Aspinall
|
defect
|
blocker
|
|
4:prover-isabelle
|
#86 |
Fix parse edit offset
|
alex heneveld
|
defect
|
blocker
|
|
1:pg-eclipse
|
#124 |
Edited text doesn't update document model
|
alex heneveld
|
defect
|
blocker
|
|
1:pg-eclipse
|
#126 |
Repair symbol handling
|
David Aspinall
|
defect
|
blocker
|
|
1:pg-eclipse
|
#156 |
closing an active editor doesn't work (buggy or confusing PGRetargetableAction.setBusy())
|
David Aspinall
|
defect
|
blocker
|
|
1:pg-eclipse
|
#220 |
Remove X-Symbol, XEmacs support and backward compatibility
|
David Aspinall
|
task
|
blocker
|
PG-Emacs-4.0
|
2:pg-emacs
|
#241 |
Fix link parse and undo for <whitespace> elements.
|
David Aspinall
|
|
blocker
|
|
1:pg-eclipse
|
#245 |
Script management: parsing protocol error
|
David Aspinall
|
|
blocker
|
|
1:pg-eclipse
|
#360 |
link to proof general is broken and lacks helpful message
|
David Aspinall
|
defect
|
blocker
|
PG-Emacs-4.0
|
2:pg-emacs
|
#369 |
PG will not compile under non-windowing Emacs
|
David Aspinall
|
defect
|
blocker
|
PG-Emacs-4.0
|
2:pg-emacs
|
#502 |
Latest Makefile change breaks things everywhere except Mac
|
David Aspinall
|
defect
|
blocker
|
PG-Emacs-4.3
|
2:pg-emacs
|