Mercurial > cpdt > repo

diff src/Generic.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 e0d91bcf70ec
children 3c941750c347
line wrap: on
line diff
--- a/src/Generic.v	Mon Mar 26 16:24:19 2012 -0400
+++ b/src/Generic.v	Mon Mar 26 16:55:59 2012 -0400
@@ -586,7 +586,7 @@
 
   Restart.
 
-  Hint Rewrite hget_hmake : cpdt.
+  Hint Rewrite hget_hmake.
   Hint Resolve foldr_plus.
  
   unfold size; intros; pattern v; apply dok; crush.
@@ -605,7 +605,7 @@
 (* begin thide *)
   (** Let us begin as we did in the last theorem, after adding another useful library equality as a hint. *)
 
-  Hint Rewrite hget_hmap : cpdt.
+  Hint Rewrite hget_hmap.
 
   unfold map; intros; pattern v; apply dok; crush.
   (** %\vspace{-.15in}%[[