From 5cd9adb60e8b6e5fd1ce87adcf263c3a8b358cdc Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 11 Jul 2013 14:58:35 +0000
Subject: Fixing another bug in indentation concerning "where". Actually there
 are other uses of "where (declaring notation for records that I did no test).

---
 coq/ex/indent.v | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'coq/ex')

diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index 34286fed..c574f715 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -172,10 +172,11 @@ Class cla {X:Set}:Set := {
 
 
 Module X.
-  Lemma l :
-  forall r:rec,
-  exists r':rec,
-    r'.(fld1) = r.(fld2)/\ r'.(fld2) = r.(fld1).
+  Lemma l
+  :
+    forall r:rec,
+    exists r':rec,
+      r'.(fld1) = r.(fld2)/\ r'.(fld2) = r.(fld1).
   Proof.
     intros r.  
     { exists 
-- 
cgit v1.2.3