diff options
| author | Pierre Courtieu | 2013-07-10 15:02:11 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2013-07-10 15:02:11 +0000 |
| commit | 215dce626eb21fd0e504517d55b552f5c303dccb (patch) | |
| tree | d9d6e697040651678e491e00bd7572eb45e77f43 | |
| parent | 0d644ac0cf3c713f16a114b801de9d3f98f928f0 (diff) | |
Fixing #476 (bis). Adding Fixpoint as a goal starter.
| -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)))) |