Mercurial > cpdt > repo

comparison src/Tactics.v @ 12:bcf375310f5f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Squash book into main directory
author Adam Chlipala <adamc@hcoop.net>
date Wed, 03 Sep 2008 13:30:05 -0400
parents book/src/Tactics.v@9fea5674367c
children 6d05ee182b65
comparison
equal deleted inserted replaced
6:b22369f7f0fe 12:bcf375310f5f
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.