From ad5a025af110bd9bda1461c894ed1d0b90aa027d Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 10 Jul 2013 14:58:48 +0000
Subject: Fixing #476. Adding more keywords for indentation like Lemma.

---
 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 43901ae5..a8e7a9ce 100644
--- a/coq/coq-smie-lexer.el
+++ b/coq/coq-smie-lexer.el
@@ -231,6 +231,7 @@ force indentation."
   (save-excursion ; FIXME add other commands that potentialy open goals
     (when (proof-looking-at "\\(Local\\|Global\\)?\
 \\(Definition\\|Lemma\\|Theorem\\|Fact\\|Let\\|Class\
+\\|Proposition\\|Remark\\|Instance\\|Corollary\\|Goal\
 \\|Add\\(\\s-+Parametric\\)?\\s-+Morphism\\)\\>")
 	(coq-lonely-:=-in-this-command))))
 
@@ -468,7 +469,7 @@ The point should be at the beginning of the command name."
 	   (save-excursion
 	     (not (member
 		   (coq-smie-backward-token) ;; recursive call looking at the ptoken immediately before
-		   '("." ". proofstart" "; tactic" "[" "]" "|" "=>" ;; => may be wrong here but rare (have "=> ltac"?)
+		   '("." ". proofstart" "; tactic" "[" "]" "|" "=>" ;; => may be wrong here but rare (h0ave "=> ltac"?)
 		     "{ subproof" "} subproof" "- bullet" "+ bullet"
 		     "* bullet")))))
       "quantif exists")
-- 
cgit v1.2.3