diff options
| -rw-r--r-- | coq/coq-smie-lexer.el | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/coq/coq-smie-lexer.el b/coq/coq-smie-lexer.el index a8e7a9ce..10d278c3 100644 --- a/coq/coq-smie-lexer.el +++ b/coq/coq-smie-lexer.el @@ -232,7 +232,8 @@ force indentation." (when (proof-looking-at "\\(Local\\|Global\\)?\ \\(Definition\\|Lemma\\|Theorem\\|Fact\\|Let\\|Class\ \\|Proposition\\|Remark\\|Instance\\|Corollary\\|Goal\ -\\|Add\\(\\s-+Parametric\\)?\\s-+Morphism\\)\\>") +\\|Add\\(\\s-+Parametric\\)?\\s-+Morphism\ +\\|Fixpoint\\)\\>") ;; Yes Fixpoint can start a proof like Definition (coq-lonely-:=-in-this-command)))) |