Mercurial > cpdt > repo

diff src/Tactics.v @ 35:6d05ee182b65

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nested Inductive Types
author Adam Chlipala <adamc@hcoop.net>
date Wed, 10 Sep 2008 15:47:22 -0400
parents bcf375310f5f
children 95e24b629ad9
line wrap: on
line diff
--- a/src/Tactics.v	Wed Sep 10 14:41:41 2008 -0400
+++ b/src/Tactics.v	Wed Sep 10 15:47:22 2008 -0400
@@ -21,6 +21,6 @@
 
 Hint Rewrite app_ass : cpdt.
 
-Ltac sintuition := simpl; intuition.
+Ltac sintuition := simpl in *; intuition.
 
 Ltac crush := sintuition; rewriter; sintuition.