Mercurial > cpdt > repo
changeset 80:506a06118014
Try arithmetic contradiction
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 04 Oct 2008 14:58:00 -0400 |
parents | 6c2607211cee |
children | f295a64bf9fd |
files | src/Tactics.v |
diffstat | 1 files changed, 1 insertions(+), 1 deletions(-) [+] |
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.