Mercurial > cpdt > repo

comparison src/GeneralRec.v @ 547:2c8c693ddaba

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixes for Coq 8.6
author Adam Chlipala <adam@chlipala.net>
date Wed, 12 Jul 2017 13:08:24 -0400
parents ed829eaa91b2
children a43fd2ba7ad3
comparison
equal deleted inserted replaced
546:306539f29eea 547:2c8c693ddaba
820 -> exec (Bnd m (fun x => Bnd (f x) g)) r. 820 -> exec (Bnd m (fun x => Bnd (f x) g)) r.
821 induction 1; crush. 821 induction 1; crush.
822 match goal with 822 match goal with
823 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst 823 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
824 end. 824 end.
825 move H3 after A.
826 generalize dependent B0.
827 do 2 intro.
828 subst.
829 crush. 825 crush.
830 inversion H; clear H; crush. 826 inversion H; clear H; crush.
831 eauto. 827 eauto.
832 Qed. 828 Qed.
833 829
837 -> exec (Bnd (Bnd m f) g) r. 833 -> exec (Bnd (Bnd m f) g) r.
838 induction 1; crush. 834 induction 1; crush.
839 match goal with 835 match goal with
840 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst 836 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
841 end. 837 end.
842 move H3 after B.
843 generalize dependent B0.
844 do 2 intro.
845 subst.
846 crush. 838 crush.
847 inversion H0; clear H0; crush. 839 inversion H0; clear H0; crush.
848 eauto. 840 eauto.
849 Qed. 841 Qed.
850 842