Mercurial > cpdt > repo

diff src/CpdtTactics.v @ 375:d1276004eec9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish pass over LogicProg; change [crush] to take advantage of new [Hint Rewrite] syntax that uses database [core] by default
author Adam Chlipala <adam@chlipala.net>
date Mon, 26 Mar 2012 16:55:59 -0400
parents d5787b70cf48
children 76e1dfcb86eb
line wrap: on
line diff
--- a/src/CpdtTactics.v	Mon Mar 26 16:24:19 2012 -0400
+++ b/src/CpdtTactics.v	Mon Mar 26 16:55:59 2012 -0400
@@ -81,11 +81,11 @@
     | [ H : _ |- _ ] => rewrite H; auto; [idtac]
   end.
 
-Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *).
+Ltac rewriterP := repeat (rewriteHyp; autorewrite with core in *).
 
-Ltac rewriter := autorewrite with cpdt in *; rewriterP.
+Ltac rewriter := autorewrite with core in *; rewriterP.
 
-Hint Rewrite app_ass : cpdt.
+Hint Rewrite app_ass.
 
 Definition done (T : Type) (x : T) := True.
 
@@ -130,7 +130,7 @@
 
 Ltac crush' lemmas invOne :=
   let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in
-    let rewriter := autorewrite with cpdt in *;
+    let rewriter := autorewrite with core in *;
       repeat (match goal with
                 | [ H : ?P |- _ ] =>
                   match P with
@@ -139,7 +139,7 @@
                       || (rewrite H; [ | solve [ crush' lemmas invOne ] ])
                         || (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ])
                   end
-              end; autorewrite with cpdt in *)
+              end; autorewrite with core in *)
     in (sintuition; rewriter;
         match lemmas with
           | false => idtac