Mercurial > cpdt > repo
diff src/GeneralRec.v @ 375:d1276004eec9
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 | b01c7b3122cc |
| children | 31fa03bc0f18 |
line wrap: on
line diff
--- a/src/GeneralRec.v Mon Mar 26 16:24:19 2012 -0400 +++ b/src/GeneralRec.v Mon Mar 26 16:55:59 2012 -0400 @@ -696,7 +696,7 @@ simpl; findDestr; reflexivity. Qed. -Hint Rewrite TBind_Answer : cpdt. +Hint Rewrite TBind_Answer. (** printing exists $\exists$ *) @@ -723,7 +723,7 @@ | EvalAnswer : forall x, eval (Answer x) x | EvalThink : forall m x, eval m x -> eval (Think m) x. -Hint Rewrite frob_eq : cpdt. +Hint Rewrite frob_eq. Lemma eval_frob : forall A (c : thunk A) x, eval (frob c) x