From a86143f025aaa4c62ec2621df7ebe3363c251cb4 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 24 Dec 2014 01:32:07 +0000
Subject: fixing a small pb in indentation of arrow (->). Not perfect.

---
 coq/coq-smie.el | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index fcc2ff83..dd0d584c 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -448,6 +448,17 @@ The point should be at the beginning of the command name."
 		"; tactic"
 	      "; record"))))))
 
+     ; Same for "->" : rewrite or intro arg or term's implication
+     ; FIXME: user defined arrows will be considered a term
+     ((equal tok "->")
+      (save-excursion
+	(let ((backtok (coq-smie-search-token-backward '("intro" "intros" "rewrite" "."))))
+	  (cond
+	   ((equal backtok ".") "->")
+	   ((equal backtok nil) "->")
+	   (t "-> tactic")))))
+
+
      ((equal tok "Module")
       (save-excursion
 	;(coq-find-real-start)
@@ -503,13 +514,11 @@ The point should be at the beginning of the command name."
 	   (save-excursion
 	     ;; recursive call looking at the ptoken immediately before
 	     (let ((prevtok (coq-smie-backward-token)))
-	        ;; => may be wrong here but rare (have "=> ltac"?)
+	       ;; => may be wrong here but rare (have "=> ltac"?)
 	       (not (or (coq-is-cmdend-token prevtok)
 			(member prevtok '("; tactic" "[" "]" "|" "=>")))))))
       "quantif exists")
 
-
-
      ((equal tok "∀") "forall")
      ((equal tok "→") "->")
      ((equal tok "∨") "\\/")
@@ -517,7 +526,7 @@ The point should be at the beginning of the command name."
 
      ((equal tok "with") ; "with" is a nightmare: at least 4 different uses
       (save-excursion (coq-smie-with-deambiguate)))
-     ((equal tok "where") ; "with" is a nightmare: at least 4 different uses
+     ((equal tok "where")
       "where")
 
      ((and (equal tok "signature")
-- 
cgit v1.2.3