Mercurial > cpdt > repo

diff src/Coinductive.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 549d604c3d16
children eb0fa506d04c
line wrap: on
line diff
--- a/src/Coinductive.v	Mon Mar 26 16:24:19 2012 -0400
+++ b/src/Coinductive.v	Mon Mar 26 16:55:59 2012 -0400
@@ -619,7 +619,7 @@
             end; crush).
 Qed.
 
-Hint Rewrite optExp_correct : cpdt.
+Hint Rewrite optExp_correct .
 
 (** The final theorem is easy to establish, using our co-induction principle and a bit of Ltac smarts that we leave unexplained for now.  Curious readers can consult the Coq manual, or wait for the later chapters of this book about proof automation. *)