Mercurial > cpdt > repo

comparison src/Tactics.v @ 173:7fd470d8a788

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
System F
author Adam Chlipala <adamc@hcoop.net>
date Sun, 09 Nov 2008 15:15:41 -0500
parents 56e205f966cc
children 9b1f58dbc464
comparison
equal deleted inserted replaced
172:653c03f6061e 173:7fd470d8a788
159 generalize (UIP_refl _ _ Heq); intro; subst; clear Heq 159 generalize (UIP_refl _ _ Heq); intro; subst; clear Heq
160 | [ Heq : ?E = _ |- _ ] => bestEffort Heq E ltac:(fun E => rewrite E) 160 | [ Heq : ?E = _ |- _ ] => bestEffort Heq E ltac:(fun E => rewrite E)
161 | [ Heq : _ = ?E |- _ ] => bestEffort Heq E ltac:(fun E => rewrite <- E) 161 | [ Heq : _ = ?E |- _ ] => bestEffort Heq E ltac:(fun E => rewrite <- E)
162 end 162 end
163 in match type of E with 163 in match type of E with
164 | _ ?A => doit A
164 | _ _ ?A => doit A 165 | _ _ ?A => doit A
165 | _ ?A => doit A 166 | _ _ _ ?A => doit A
166 end. 167 end.
167 168
168 Ltac clear_all := 169 Ltac clear_all :=
169 repeat match goal with 170 repeat match goal with
170 | [ H : _ |- _ ] => clear H 171 | [ H : _ |- _ ] => clear H