Mercurial > cpdt > repo

comparison src/DataStruct.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 05efde66559d
comparison
equal deleted inserted replaced
374:f3146d40c2a1 375:d1276004eec9
836 (* end thide *) 836 (* end thide *)
837 837
838 Theorem cfold_correct : forall t (e : exp' t), 838 Theorem cfold_correct : forall t (e : exp' t),
839 exp'Denote (cfold e) = exp'Denote e. 839 exp'Denote (cfold e) = exp'Denote e.
840 (* begin thide *) 840 (* begin thide *)
841 Hint Rewrite cfoldCond_correct : cpdt. 841 Hint Rewrite cfoldCond_correct.
842 Hint Resolve cond_ext. 842 Hint Resolve cond_ext.
843 843
844 induction e; crush; 844 induction e; crush;
845 repeat (match goal with 845 repeat (match goal with
846 | [ |- context[cfold ?E] ] => dep_destruct (cfold E) 846 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)