From 215dce626eb21fd0e504517d55b552f5c303dccb Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 10 Jul 2013 15:02:11 +0000
Subject: Fixing #476 (bis). Adding Fixpoint as a goal starter.

---
 coq/coq-smie-lexer.el | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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))))
 
 
-- 
cgit v1.2.3