Mercurial > cpdt > repo
diff src/Tactics.v @ 64:739c2818d6e2
Co-inductive evaluation example
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 30 Sep 2008 17:47:59 -0400 |
| parents | 1a664ff9d2d1 |
| children | 21bb59c56b98 |
line wrap: on
line diff
--- a/src/Tactics.v Tue Sep 30 17:07:57 2008 -0400 +++ b/src/Tactics.v Tue Sep 30 17:47:59 2008 -0400 @@ -103,7 +103,7 @@ end. Ltac crush' lemmas invOne := - let sintuition := simpl in *; intuition; repeat (simplHyp invOne; intuition); try congruence + let sintuition := simpl in *; intuition; subst; repeat (simplHyp invOne; intuition; subst); try congruence in (sintuition; rewriter; repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); repeat (simplHyp invOne; intuition));