From 21ee11059cb76f7f1932616c5a753f93a1bb889d Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Sun, 3 Jun 2012 09:46:07 +0000
Subject: Fix a bug of indentation.

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

diff --git a/coq/coq.el b/coq/coq.el
index 259d7f27..5b002006 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -367,7 +367,8 @@ Lemma foo: forall n,
              ("{" exps "}")
              ("[" expssss "]")
              (exp "->" exp)
-             (exp ":" exp))
+             (exp ":" exp)
+             (exp ".-selector" exp))
         ;; Having "return" here rather than as a separate rule in `exp' causes
         ;; it to be indented at a different level than "with".
         (matchexp (matchexp "return" exp) (exp "in" exp)) ;(exp "as" exp)
diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index 752bc4f9..28a56515 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -170,11 +170,14 @@ Module X.
       {auto. }
     }
   Qed.
-
-
+  
+  
   Lemma l2 :
     forall r:rec,
-    exists r':rec,r'.(fld1) = r.(fld2) /\ r'.(fld2) = r.(fld1).
+    exists r':rec,r'.(fld1)
+                       = r.(fld2)
+                             /\ r'.(fld2)
+                                     = r.(fld1).
   Proof.
     intros r.  
     {{
-- 
cgit v1.2.3