Mercurial > cpdt > repo

changeset 189:0198181d1b64

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Automated CcExp_correct
author Adam Chlipala <adamc@hcoop.net>
date Mon, 17 Nov 2008 10:36:02 -0500
parents aec05464fedd
children 094bd1e353dd
files src/Intensional.v
diffstat 1 files changed, 8 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- 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.