From b3af77749ed07f58316371c456e78c8d7aca1505 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Mon, 4 Jun 2012 16:07:15 +0000
Subject: One more fix for indentation.

---
 coq/coq.el      | 5 ++++-
 coq/ex/indent.v | 9 +++++----
 2 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index ff243823..aaa69d3d 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -366,6 +366,8 @@ Lemma foo: forall n,
              ("{|" exps "|}")
              ("{" exps "}")
              ("[" expssss "]")
+             (exp "<->" exp)
+             (exp "=" exp)
              (exp "->" exp)
              (exp ":" exp))
         ;; Having "return" here rather than as a separate rule in `exp' causes
@@ -409,7 +411,8 @@ Lemma foo: forall n,
               ;; stops right before the "." rather than right after.
               (cmds "." cmds)))
       ;; Resolve the "trailing expression ambiguity" as in "else x -> b".
-      '((assoc ",") (nonassoc "as") (assoc ":") (assoc "->") (nonassoc "else")
+      '((assoc ",") (nonassoc "as") (assoc ":") (assoc "->")
+        (assoc "=") (assoc "<->") (nonassoc "else")
         (nonassoc "in") (assoc "in tactic") (left "=>"))
       '((assoc ",")(assoc ";")(assoc "|")(left "=>"))
       '((left "- bullet") (left "+ bullet") (left "* bullet"))
diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index 28a56515..a6fda706 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -174,10 +174,11 @@ Module X.
   
   Lemma l2 :
     forall r:rec,
-    exists r':rec,r'.(fld1)
-                       = r.(fld2)
-                             /\ r'.(fld2)
-                                     = r.(fld1).
+    exists r':rec,
+      ressai.(fld1)
+            = r.(fld2)
+            /\ r'.(fld2)
+            = r.(fld1).
   Proof.
     intros r.  
     {{
-- 
cgit v1.2.3