Mercurial > cpdt > repo

diff src/Tactics.v @ 38:95e24b629ad9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Exercises
author Adam Chlipala <adamc@hcoop.net>
date Fri, 12 Sep 2008 16:55:37 -0400
parents 6d05ee182b65
children a21eb02cc7c6
line wrap: on
line diff
--- a/src/Tactics.v	Fri Sep 12 15:30:59 2008 -0400
+++ b/src/Tactics.v	Fri Sep 12 16:55:37 2008 -0400
@@ -9,6 +9,8 @@
 
 Require Import List.
 
+Require Omega.
+
 
 Ltac rewriteHyp :=
   match goal with
@@ -23,4 +25,4 @@
 
 Ltac sintuition := simpl in *; intuition.
 
-Ltac crush := sintuition; rewriter; sintuition.
+Ltac crush := sintuition; rewriter; sintuition; try omega.