Mercurial > cpdt > repo
comparison src/GeneralRec.v @ 554:93471096cdd4
Merge
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sat, 19 Aug 2017 12:14:40 -0400 |
parents | 16d701d4bd82 |
children | af97676583f3 |
comparison
equal
deleted
inserted
replaced
553:cb81f74d8c92 | 554:93471096cdd4 |
---|---|
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. | 825 try subst B. (* This line expected to fail in Coq 8.4 and succeed in Coq 8.6. *) |
826 generalize dependent B0. | |
827 do 2 intro. | |
828 subst. | |
829 crush. | 826 crush. |
830 inversion H; clear H; crush. | 827 inversion H; clear H; crush. |
831 eauto. | 828 eauto. |
832 Qed. | 829 Qed. |
833 | 830 |
837 -> exec (Bnd (Bnd m f) g) r. | 834 -> exec (Bnd (Bnd m f) g) r. |
838 induction 1; crush. | 835 induction 1; crush. |
839 match goal with | 836 match goal with |
840 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst | 837 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst |
841 end. | 838 end. |
842 move H3 after B. | 839 try subst A. (* Same as above *) |
843 generalize dependent B0. | |
844 do 2 intro. | |
845 subst. | |
846 crush. | 840 crush. |
847 inversion H0; clear H0; crush. | 841 inversion H0; clear H0; crush. |
848 eauto. | 842 eauto. |
849 Qed. | 843 Qed. |
850 | 844 |