Mercurial > cpdt > repo
diff src/Tactics.v @ 183:02569049397b
Closure conversion defined
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 16 Nov 2008 14:01:33 -0500 |
| parents | 8f3fc56b90d4 |
| children | 699fd70c04a7 |
line wrap: on
line diff
--- a/src/Tactics.v Sun Nov 16 11:54:51 2008 -0500 +++ b/src/Tactics.v Sun Nov 16 14:01:33 2008 -0500 @@ -72,7 +72,7 @@ Ltac rewriteHyp := match goal with - | [ H : _ |- _ ] => rewrite H + | [ H : _ |- _ ] => rewrite H; auto; [idtac] end. Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *). @@ -122,12 +122,17 @@ Ltac crush' lemmas invOne := let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence - in (sintuition; rewriter; - match lemmas with - | false => idtac - | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); - repeat (simplHyp invOne; intuition)); un_done - end; sintuition; try omega; try (elimtype False; omega)). + in (sintuition; + autorewrite with cpdt in *; + repeat (match goal with + | [ H : _ |- _ ] => (rewrite H; []) + || (rewrite H; [ | solve [ crush' lemmas invOne ] ]) + end; autorewrite with cpdt in *); + match lemmas with + | false => idtac + | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); + repeat (simplHyp invOne; intuition)); un_done + end; sintuition; try omega; try (elimtype False; omega)). Ltac crush := crush' false fail.