1 files changed, 5 insertions, 4 deletions
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