From 353b3c6a4ecb9b72aa28e02db4374f9d94151e14 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Sun, 10 Jun 2012 10:40:59 +0000
Subject: Fixing indentation details for coq.

---
 coq/coq.el | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index fb3bdcd4..ea467d37 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -363,12 +363,11 @@ Lemma foo: forall n,
              ("quantif exists" exp "," exp)
              ("forall" exp "," exp)
              ("(" exps ")") ("{|" exps "|}") ("{" exps "}") ("[" expssss "]")
-             (exp "<->" exp) (exp "/\\" exp) (exp "\\/" exp)
-             (exp "==" exp) (exp "^" exp) (exp "+" exp)
-             (exp "-" exp) (exp "*" exp) ;(exp "/" exp)
-             (exp "=" exp) (exp "<>" exp) (exp "<=" exp) (exp "<" exp)
-             (exp ">=" exp) (exp ">" exp) (exp "=?" exp) (exp "<=?" exp)
-             (exp "<?" exp) (exp "->" exp)
+             (exp "->" exp) (exp "<->" exp) (exp "/\\" exp) (exp "\\/" exp)
+             (exp "==" exp) (exp "=" exp) (exp "<>" exp) (exp "<=" exp)
+             (exp "<" exp) (exp ">=" exp) (exp ">" exp)
+             (exp "=?" exp) (exp "<=?" exp) (exp "<?" exp)
+             (exp "^" exp) (exp "+" exp) (exp "-" exp) (exp "*" exp)
              (exp ":" exp))
         ;; Having "return" here rather than as a separate rule in `exp' causes
         ;; it to be indented at a different level than "with".
@@ -414,13 +413,15 @@ Lemma foo: forall n,
               (cmds "." cmds)))
       ;; Resolve the "trailing expression ambiguity" as in "else x -> b".
       ;; each line orders tokens by increasing proprity
-      '((left ",") (assoc ":") (assoc "->") (left "<->")
+      '((left ",") (assoc ":")
+        (assoc "\\/") (assoc "/\\") 
+        (assoc "->") (left "<->")
         (assoc "<?") (assoc "<=?") (assoc "=?") (assoc ">") (assoc ">=")
         (assoc "<") (assoc "<=") (left "<>") (left "=") (left "==")
         (nonassoc "else") (nonassoc "in") (assoc "in tactic")
         (assoc ":= record") (assoc "; record") (left "=>")
         (left "^")
-        (assoc "-")(assoc "+") (assoc "\\/") (assoc "*") (assoc "/\\"))
+        (assoc "-")(assoc "+") (assoc "*") )
       '((left ",")(assoc ";")(right "as")(left "|")(left "=>"))
       '((left "- bullet") (left "+ bullet") (left "* bullet"))
       '((assoc ".")))))
-- 
cgit v1.2.3