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