From 470ea050b6cfa3b96f4eb5721d36d6f56e2588bb Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 25 Jan 2008 15:26:11 +0000
Subject: Updated.

---
 etc/coq/indent.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/etc/coq/indent.v b/etc/coq/indent.v
index 46839715..be27f9ef 100644
--- a/etc/coq/indent.v
+++ b/etc/coq/indent.v
@@ -64,5 +64,5 @@ Theorem p : forall (P : Prop), P -> P.
 Proof.
   try (simpl 
     in *). 
-  intros P H. apply H.
+    intros P H. apply H.  (* da: shouldn't we outdent again here? *)
 Qed.
-- 
cgit v1.2.3