Mercurial > cpdt > repo
comparison book/src/Tactics.v @ 3:9fea5674367c
Pretty LaTeX generation
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 29 Aug 2008 14:24:38 -0400 |
parents | book/Tactics.v@b3f7de74d38f |
children |
comparison
equal
deleted
inserted
replaced
2:b3f7de74d38f | 3:9fea5674367c |
---|---|
1 (* Copyright (c) 2008, Adam Chlipala | |
2 * | |
3 * This work is licensed under a | |
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 | |
5 * Unported License. | |
6 * The license text is available at: | |
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ | |
8 *) | |
9 | |
10 Require Import List. | |
11 | |
12 | |
13 Ltac rewriteHyp := | |
14 match goal with | |
15 | [ H : _ |- _ ] => rewrite H | |
16 end. | |
17 | |
18 Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *). | |
19 | |
20 Ltac rewriter := autorewrite with cpdt in *; rewriterP. | |
21 | |
22 Hint Rewrite app_ass : cpdt. | |
23 | |
24 Ltac sintuition := simpl; intuition. | |
25 | |
26 Ltac crush := sintuition; rewriter; sintuition. |