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 :=