## Mercurial > cpdt > repo

### comparison src/GeneralRec.v @ 549:16d701d4bd82

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

And working with 8.6 again

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Wed, 12 Jul 2017 13:49:46 -0400 |

parents | a43fd2ba7ad3 |

children | af97676583f3 |

comparison

equal
deleted
inserted
replaced

548:a43fd2ba7ad3 | 549:16d701d4bd82 |
---|---|

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 subst B. | 825 try subst B. (* This line expected to fail in Coq 8.4 and succeed in Coq 8.6. *) |

826 crush. | 826 crush. |

827 inversion H; clear H; crush. | 827 inversion H; clear H; crush. |

828 eauto. | 828 eauto. |

829 Qed. | 829 Qed. |

830 | 830 |

834 -> exec (Bnd (Bnd m f) g) r. | 834 -> exec (Bnd (Bnd m f) g) r. |

835 induction 1; crush. | 835 induction 1; crush. |

836 match goal with | 836 match goal with |

837 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst | 837 | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst |

838 end. | 838 end. |

839 subst A. | 839 try subst A. (* Same as above *) |

840 crush. | 840 crush. |

841 inversion H0; clear H0; crush. | 841 inversion H0; clear H0; crush. |

842 eauto. | 842 eauto. |

843 Qed. | 843 Qed. |

844 | 844 |