Mercurial > cpdt > repo

annotate src/Tactics.v @ 41:d45ba7e9b266

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Improve template generation; craft template for InductiveTypes
author Adam Chlipala <adamc@hcoop.net>
date Sat, 13 Sep 2008 14:31:51 -0400
parents 95e24b629ad9
children a21eb02cc7c6
rev   line source
adamc@2 1 (* Copyright (c) 2008, Adam Chlipala
adamc@2 2 *
adamc@2 3 * This work is licensed under a
adamc@2 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@2 5 * Unported License.
adamc@2 6 * The license text is available at:
adamc@2 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@2 8 *)
adamc@2 9
adamc@2 10 Require Import List.
adamc@2 11
adamc@38 12 Require Omega.
adamc@38 13
adamc@2 14
adamc@2 15 Ltac rewriteHyp :=
adamc@2 16 match goal with
adamc@2 17 | [ H : _ |- _ ] => rewrite H
adamc@2 18 end.
adamc@2 19
adamc@2 20 Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *).
adamc@2 21
adamc@2 22 Ltac rewriter := autorewrite with cpdt in *; rewriterP.
adamc@2 23
adamc@2 24 Hint Rewrite app_ass : cpdt.
adamc@2 25
adamc@35 26 Ltac sintuition := simpl in *; intuition.
adamc@2 27
adamc@38 28 Ltac crush := sintuition; rewriter; sintuition; try omega.