Custom Query (361 matches)
Results (1 - 3 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #160 | fixed | "Abort" keyword not recognized in Coq | ||
| Description |
Indentation is not closed properly after an "Abort." statement, following "Theorem". Simple fix: In coq/coq-syntax.el: Add "Abort" to the list of keywords defined in coq-keywords-save-strict (line 618 in ProofGeneral-3.7pre071025). |
|||
| #431 | needmoreinfo | "This subproof is complete" appears at bottom of goals | ||
| Description |
After a bulleted subproof has been completed, This subproof is complete, but there are still unfocused goals: appears at the bottom of the goals window. It should either appear at the top, or not at all. |
|||
| #485 | fixed | "Time commands" option offsets the cursor when errors are reported | ||
| Description |
When activating the "Time Commands" option, every time an error is displayed, the cursor is off 5 characters to the right. Happens in the latest development build as well as in the last stable. To reproduce, open a buffer and type: Inductive t := T : x -> y -> t.
Try to run it when "Time Commands" is on. The error is reported on the |
|||
