Custom Query (361 matches)


Show under each result:

Results (1 - 3 of 361)

1 2 3 4 5 6 7 8 9 10 11
Ticket Resolution Summary Owner Reporter
#160 fixed "Abort" keyword not recognized in Coq David Aspinall scsibug

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 David Aspinall Robin Green

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 David Aspinall coquser

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 t character instead of the y character.

1 2 3 4 5 6 7 8 9 10 11
Note: See TracQuery for help on using queries.