Try arithmetic contradiction

36f51ef2 · Adam Chlipala · bc9ad81d · 36f51ef2
Commit 36f51ef2 authored Oct 04, 2008 by Adam Chlipala
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

Tactics.v src/Tactics.v +1 -1

No files found.
--- a/src/Tactics.v
+++ b/src/Tactics.v
@@ -112,6 +112,6 @@ Ltac crush' lemmas invOne :=
    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.