#391 |
proof-full-annotation causes instabilities
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#392 |
Isabelle anti-quotation colouring obliterates symbol font setting
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.2
|
2:pg-emacs
|
#394 |
Coq "Library" keyword - incorrect coloring
|
courtieu
|
defect
|
trivial
|
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
|
#396 |
error in proof-shell-insert-hook docstring
|
David Aspinall
|
defect
|
trivial
|
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
|
#399 |
dvi target in doc/Makefile.doc missing
|
David Aspinall
|
defect
|
minor
|
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
|
#402 |
Clean up customization groups/settings
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.2
|
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
|
#405 |
Report Emacs bug: Quail input breaks delete-char behaviour
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#406 |
auto compile bugs when some outputs is done by coqc
|
coquser
|
defect
|
critical
|
PG-Emacs-4.2
|
2:pg-emacs
|
#407 |
proof-undo-and-delete-last-successful-command does not meet spec
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#408 |
Auto compile fails if coq-compile-response-buffer has been killed
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#409 |
Problem with wide unicode characters in emacs 23.3
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#410 |
coq parsing broken since Jun 04 20:12:40
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#411 |
wiki formatting corrupts tickets
|
David Aspinall
|
defect
|
minor
|
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
|
#413 |
Clicking on Find icon does not bring up input buffer
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.1
|
2:pg-emacs
|
#414 |
PG thinks Preterm command is not state-preserving
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-4.1
|
2:pg-emacs
|
#415 |
Wrong file mentioned in installation notes
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-4.1
|
6:web-and-docs
|
#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
|
#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
|
#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
|
#427 |
defpacustom and undo
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.2
|
2:pg-emacs
|
#428 |
subsubsection links not working in PG doc
|
David Aspinall
|
defect
|
critical
|
PG-Emacs-4.2
|
2:pg-emacs
|
#431 |
"This subproof is complete" appears at bottom of goals
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-4.2
|
7:prover-coq
|
#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
|
#438 |
Startup failure on Emacs 23
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#439 |
Hang on open bracket
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
7:prover-coq
|
#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
|
#442 |
Emacs 24 and long inputs
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
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
|
#445 |
Proof General (or coqtop?) barfs on "Arguments foo / ..."
|
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
|
#447 |
Proof General stalls on long Ltac (Coq)
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
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
|
#453 |
Sending too-large definitions gets stuck
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.2
|
2:pg-emacs
|
#455 |
Emacs trunk BZR sometimes hangs when using auto fill mode with PG Coq
|
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
|
#459 |
Can not split the window vertically
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#460 |
proof general hanging on Coq Definition in file generated by Why3
|
hendrik
|
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
|
#468 |
Some notations with periods make PG hang
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#469 |
coqgeneral 4.3pre130327 does not compile with Emacs 24.3
|
David Aspinall
|
defect
|
blocker
|
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
|
#491 |
Print Implicit not available as emacs command
|
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
|
#493 |
ProofGeneral stalls/loops on ...
|
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
|
#495 |
Goals buffer aggressively cleared with Coq pre-8.5
|
David Aspinall
|
defect
|
minor
|
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
|
#511 |
new Coq command "From" supported by PG?
|
David Aspinall
|
defect
|
blocker
|
PG-Emacs-4.4
|
2:pg-emacs
|
#512 |
test.coq target doesn't exist
|
David Aspinall
|
defect
|
major
|
PG-Emacs-4.3
|
2:pg-emacs
|
#1 |
Try to get trac working for Proof General web
|
David Aspinall
|
enhancement
|
major
|
|
6:web-and-docs
|
#4 |
Use stixfonts once they become available
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-4.3
|
1:pg-eclipse
|
#6 |
Add code folding for proof scripts
|
David Aspinall
|
enhancement
|
major
|
|
1:pg-eclipse
|
#7 |
Finish proof explorer: inherit decorators, menus, etc. from Project Explorer.
|
Graham Dutton
|
enhancement
|
major
|
|
1:pg-eclipse
|
#36 |
Split stream for console into input/output and give input a different colour.
|
David Aspinall
|
enhancement
|
minor
|
|
1:pg-eclipse
|
#63 |
Improve symbols: fill out default table, add ascii-symbol completion
|
David Aspinall
|
enhancement
|
major
|
|
1:pg-eclipse
|
#71 |
Add Error Decoration to documents; optimise Active Script Decoration
|
Graham Dutton
|
enhancement
|
major
|
|
1:pg-eclipse
|
#78 |
Preferences: support dynamically computed defaults
|
David Aspinall
|
enhancement
|
trivial
|
|
1:pg-eclipse
|
#103 |
Add ASCII markup communication for Coq (fix UTF8 stream/FAQ no.1)
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-3.7
|
7:prover-coq
|
#115 |
Isabelle find-theorems form
|
David Aspinall
|
enhancement
|
major
|
PG-Emacs-3.7
|
2:pg-emacs
|