Mercurial > cpdt > repo

changeset 80:506a06118014

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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.