Mercurial > cpdt > repo

comparison src/GeneralRec.v @ 568:81d63d9c1cc5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port to Coq 8.9.0
author Adam Chlipala <adam@chlipala.net>
date Sun, 20 Jan 2019 15:16:29 -0500
parents af97676583f3
children a913f19955e2
comparison
equal deleted inserted replaced
567:ec0ce5129fc4 568:81d63d9c1cc5
652 | Think m1', _ => P m1' m2 652 | Think m1', _ => P m1' m2
653 | _, Think m2' => P m1 m2' 653 | _, Think m2' => P m1 m2'
654 end. 654 end.
655 655
656 Theorem thunk_eq_coind : forall m1 m2, P m1 m2 -> thunk_eq m1 m2. 656 Theorem thunk_eq_coind : forall m1 m2, P m1 m2 -> thunk_eq m1 m2.
657 cofix; intros; 657 cofix thunk_eq_coind; intros;
658 match goal with 658 match goal with
659 | [ H' : P _ _ |- _ ] => specialize (H H'); clear H' 659 | [ H' : P _ _ |- _ ] => specialize (H H'); clear H'
660 end; destruct m1; destruct m2; subst; repeat constructor; auto. 660 end; destruct m1; destruct m2; subst; repeat constructor; auto.
661 Qed. 661 Qed.
662 End thunk_eq_coind. 662 End thunk_eq_coind.