# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1226936162 18000
# Node ID 0198181d1b647bb86e7bceffbe7a541979cc8697
# Parent  aec05464feddf27bb58f135e51185f6ead31da51
Automated CcExp_correct

diff -r aec05464fedd -r 0198181d1b64 src/Intensional.v
--- a/src/Intensional.v	Mon Nov 17 10:31:22 2008 -0500
+++ b/src/Intensional.v	Mon Nov 17 10:36:02 2008 -0500
@@ -1044,20 +1044,18 @@
       -> wfExp fvs e1.
     Hint Extern 3 (Some _ = Some _) => elimtype False; eapply lookup_bound_contra; eauto.
 
-    induction 1; crush.
-    eapply H0.
-    eauto.
-
-    apply H0 with (length envT).
-    my_crush.
-    eauto.
+    induction 1; crush; eauto;
+      match goal with
+        | [ H : _, envT : list Source.type |- _ ] =>
+          apply H with (length envT); my_crush; eauto
+      end.
   Qed.
 
   Theorem Exp_wf : forall t (E : Source.Exp t),
     wfExp (envT := nil) tt (E _).
-    intros; eapply Exp_wf';
-      [apply Exp_equiv
-        | crush].
+    Hint Resolve Exp_equiv.
+
+    intros; eapply Exp_wf'; crush.
   Qed.
 End wf.