From 8be536fe303eb1061aee731a9830e577b4656ef9 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 29 May 2013 15:59:04 +0000
Subject: Fixing a minor bug in indetation (exists is tactic and a quantifier).

---
 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 a3522b69..6a71cda8 100644
--- a/coq/coq-smie-lexer.el
+++ b/coq/coq-smie-lexer.el
@@ -463,7 +463,8 @@ The point should be at the beginning of the command name."
 	     (not (member
 		   (coq-smie-backward-token) ;; recursive call
 		   '("." ". proofstart" "; tactic" "[" "]" "|"
-		     "{ subproof" "} subproof"))))
+		     "{ subproof" "} subproof" "- bullet" "+ bullet"
+		     "* bullet"))))
 	   "quantif exists"))
      ((equal tok "∀") "forall")
      ((equal tok "→") "->")
-- 
cgit v1.2.3