From 9442124c8204c6d8fec6fd1261fb2a19c9b6521b Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 25 Jan 2008 15:24:21 +0000
Subject: Patch and cleanup for Coq indent code, see
 http://proofgeneral.inf.ed.ac.uk/trac/ticket/173

---
 etc/coq/indent.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'etc')

diff --git a/etc/coq/indent.v b/etc/coq/indent.v
index 456018c6..46839715 100644
--- a/etc/coq/indent.v
+++ b/etc/coq/indent.v
@@ -58,5 +58,11 @@ Definition f :=
        | # => #       
        end
      end
-    
 
+(* Nasty example from Trac http://proofgeneral.inf.ed.ac.uk/trac/ticket/173 *)    
+Theorem p : forall (P : Prop), P -> P.
+Proof.
+  try (simpl 
+    in *). 
+  intros P H. apply H.
+Qed.
-- 
cgit v1.2.3