Mercurial > cpdt > repo
diff src/Tactics.v @ 80:506a06118014
Try arithmetic contradiction
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 04 Oct 2008 14:58:00 -0400 |
parents | b52204928c7d |
children | 522436ed6688 |
line wrap: on
line diff
--- a/src/Tactics.v Fri Oct 03 17:53:41 2008 -0400 +++ b/src/Tactics.v Sat Oct 04 14:58:00 2008 -0400 @@ -112,6 +112,6 @@ in (sintuition; rewriter; repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); repeat (simplHyp invOne; intuition)); - un_done; sintuition; try omega). + un_done; sintuition; try omega; try (elimtype False; omega)). Ltac crush := crush' tt fail.