Opened 16 years ago

Closed 16 years ago

#160 closed defect (fixed)

"Abort" keyword not recognized in Coq

Reported by: scsibug Owned by: David Aspinall
Priority: minor Milestone: PG-Emacs-3.7
Component: 2:pg-emacs Keywords:
Cc:

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).

Change History (2)

comment:1 Changed 16 years ago by scsibug

Actually, line 677 is where the keyword should be added. (618 without blank lines).

comment:2 Changed 16 years ago by David Aspinall

Resolution: fixed
Status: newclosed

Fix added, many thanks for report.

Note: See TracTickets for help on using tickets.