Mercurial > cpdt > repo
diff src/Tactics.v @ 173:7fd470d8a788
System F
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 09 Nov 2008 15:15:41 -0500 |
parents | 56e205f966cc |
children | 9b1f58dbc464 |
line wrap: on
line diff
--- a/src/Tactics.v Sun Nov 09 14:24:31 2008 -0500 +++ b/src/Tactics.v Sun Nov 09 15:15:41 2008 -0500 @@ -161,8 +161,9 @@ | [ Heq : _ = ?E |- _ ] => bestEffort Heq E ltac:(fun E => rewrite <- E) end in match type of E with + | _ ?A => doit A | _ _ ?A => doit A - | _ ?A => doit A + | _ _ _ ?A => doit A end. Ltac clear_all :=