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
comment:2 Changed 16 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Fix added, many thanks for report.
Note: See
TracTickets for help on using
tickets.
Actually, line 677 is where the keyword should be added. (618 without blank lines).