Custom Query (42 matches)
Resolution: fixed (32 matches)
Ticket
|
Summary
|
Owner
|
Type
|
Priority
|
Created
|
Modified
|
#512 |
test.coq target doesn't exist
|
David Aspinall
|
defect
|
major
|
8 years ago
|
8 years ago
|
#505 |
Fix indentation of lazymatch in Coq
|
cpitcla
|
enhancement
|
minor
|
9 years ago
|
9 years ago
|
#504 |
Minor fix for coq-is-symbol-or-punct and coq-grab-punctuation-left
|
cpitcla
|
enhancement
|
minor
|
9 years ago
|
9 years ago
|
#503 |
Some coq output get lost for query processed just after an error stops the queue.
|
David Aspinall
|
defect
|
minor
|
9 years ago
|
9 years ago
|
#502 |
Latest Makefile change breaks things everywhere except Mac
|
David Aspinall
|
defect
|
blocker
|
9 years ago
|
9 years ago
|
#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
|
9 years ago
|
9 years ago
|
#494 |
PG incorrectly parses the result of [Fail] in some cases
|
David Aspinall
|
defect
|
major
|
10 years ago
|
9 years ago
|
#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
|
10 years ago
|
9 years ago
|
#489 |
Electric Terminator mode breaks desktop-save-mode
|
David Aspinall
|
defect
|
minor
|
10 years ago
|
9 years ago
|
#487 |
Coq syntax highlighting: Proposition
|
David Aspinall
|
defect
|
minor
|
10 years ago
|
10 years ago
|
#485 |
"Time commands" option offsets the cursor when errors are reported
|
David Aspinall
|
defect
|
minor
|
11 years ago
|
9 years ago
|
#484 |
[Existing Instances] should be highlighted like [Existing Instance]
|
David Aspinall
|
defect
|
minor
|
11 years ago
|
9 years ago
|
#482 |
[lazymatch] should be highlighted and indented like [match]
|
David Aspinall
|
defect
|
minor
|
11 years ago
|
9 years ago
|
#479 |
[intros ??.] messes up following indentation
|
David Aspinall
|
defect
|
minor
|
11 years ago
|
9 years ago
|
#478 |
[Proof <body term>.] messes up following indentation
|
David Aspinall
|
defect
|
minor
|
11 years ago
|
11 years ago
|
#477 |
[Proposition] is not highlighted like [Lemma]
|
David Aspinall
|
defect
|
minor
|
11 years ago
|
11 years ago
|
#476 |
[Goal], [Proposition], [Intance], [Fixpoint], [Corollary] do not have indented proof scripts
|
David Aspinall
|
defect
|
minor
|
11 years ago
|
11 years ago
|
#475 |
[exists] tactic causes improper indentation
|
David Aspinall
|
defect
|
minor
|
11 years ago
|
11 years ago
|
#474 |
Indentation screwed up in sigT notations ("{ _ : _ & _ }") spanning multiple lines
|
courtieu
|
defect
|
minor
|
11 years ago
|
11 years ago
|
#473 |
Indentation screwed up by "/." (not by "/ .") in, e.g., [Arguments foo /.]
|
David Aspinall
|
defect
|
minor
|
11 years ago
|
11 years ago
|
#472 |
texi2pdf loads Proofgeneral.pdf as image
|
David Aspinall
|
defect
|
minor
|
11 years ago
|
11 years ago
|
#471 |
ProofGeneral.jpg missing in ProofGeneral-4.3pre130510.tgz
|
David Aspinall
|
defect
|
minor
|
11 years ago
|
11 years ago
|
#470 |
texinfo 5.1 incompatibility
|
David Aspinall
|
defect
|
minor
|
11 years ago
|
11 years ago
|
#467 |
The "Time (tactic)." vernacular command no longer displays timings unless the tactic finishes the proof
|
hendrik
|
defect
|
major
|
11 years ago
|
11 years ago
|
#466 |
parentheses in comments should not affect indentation level of non-comment code
|
David Aspinall
|
defect
|
minor
|
11 years ago
|
11 years ago
|
#463 |
Warning messages suppress error messages and make PG have incorrect behavior with Coq
|
David Aspinall
|
defect
|
major
|
11 years ago
|
9 years ago
|
#461 |
old manuals on website
|
David Aspinall
|
defect
|
major
|
11 years ago
|
11 years ago
|
#458 |
ProofGeneral 4.2 byte-compilation fails with Emacs 24.2.90
|
David Aspinall
|
defect
|
major
|
11 years ago
|
11 years ago
|
#452 |
Some Isabelle options enabled but not active
|
David Aspinall
|
defect
|
major
|
12 years ago
|
11 years ago
|
#451 |
support {} and bullets in prooftree
|
David Aspinall
|
defect
|
major
|
12 years ago
|
11 years ago
|
#446 |
window-live-p error (coq, aquamacs)
|
David Aspinall
|
defect
|
major
|
12 years ago
|
12 years ago
|
#434 |
phox seems completely broken
|
David Aspinall
|
defect
|
critical
|
12 years ago
|
7 years ago
|
Resolution: invalid (1 match)
|
Ticket
|
Summary
|
Owner
|
Type
|
Priority
|
Created
|
Modified
|
#495 |
Goals buffer aggressively cleared with Coq pre-8.5
|
David Aspinall
|
defect
|
minor
|
10 years ago
|
10 years ago
|
Resolution: wontfix (5 matches)
|
Ticket
|
Summary
|
Owner
|
Type
|
Priority
|
Created
|
Modified
|
#493 |
ProofGeneral stalls/loops on ...
|
David Aspinall
|
defect
|
minor
|
10 years ago
|
9 years ago
|
#491 |
Print Implicit not available as emacs command
|
David Aspinall
|
defect
|
minor
|
10 years ago
|
9 years ago
|
#468 |
Some notations with periods make PG hang
|
David Aspinall
|
defect
|
minor
|
11 years ago
|
11 years ago
|
#459 |
Can not split the window vertically
|
David Aspinall
|
defect
|
major
|
11 years ago
|
11 years ago
|
#381 |
Report Emacs bug/issue: slow process filter behaviour on non-Linux platforms
|
David Aspinall
|
task
|
minor
|
13 years ago
|
12 years ago
|
Resolution: duplicate (2 matches)
|
Ticket
|
Summary
|
Owner
|
Type
|
Priority
|
Created
|
Modified
|
#469 |
coqgeneral 4.3pre130327 does not compile with Emacs 24.3
|
David Aspinall
|
defect
|
blocker
|
11 years ago
|
11 years ago
|
#442 |
Emacs 24 and long inputs
|
David Aspinall
|
defect
|
major
|
12 years ago
|
12 years ago
|
Resolution: worksforme (1 match)
|
Ticket
|
Summary
|
Owner
|
Type
|
Priority
|
Created
|
Modified
|
#460 |
proof general hanging on Coq Definition in file generated by Why3
|
hendrik
|
defect
|
major
|
11 years ago
|
9 years ago
|
Resolution: upstream (1 match)
|
Ticket
|
Summary
|
Owner
|
Type
|
Priority
|
Created
|
Modified
|
#455 |
Emacs trunk BZR sometimes hangs when using auto fill mode with PG Coq
|
David Aspinall
|
defect
|
major
|
12 years ago
|
11 years ago
|
Note: See
TracQuery
for help on using queries.