## Mercurial > cpdt > repo

### comparison src/ProgLang.v @ 535:dac7a2705b00

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

...and back to working in 8.4 again

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

date | Wed, 05 Aug 2015 14:57:14 -0400 |

parents | ed829eaa91b2 |

children |

comparison

equal
deleted
inserted
replaced

534:ed829eaa91b2 | 535:dac7a2705b00 |
---|---|

28 | 28 |

29 Ltac ext := let x := fresh "x" in extensionality x. | 29 Ltac ext := let x := fresh "x" in extensionality x. |

30 Ltac pl := crush; repeat (match goal with | 30 Ltac pl := crush; repeat (match goal with |

31 | [ |- (fun x => _) = (fun y => _) ] => ext | 31 | [ |- (fun x => _) = (fun y => _) ] => ext |

32 | [ |- _ _ _ ?E _ = _ _ _ ?E _ ] => f_equal | 32 | [ |- _ _ _ ?E _ = _ _ _ ?E _ ] => f_equal |

33 | [ |- ?E ::: _ = ?E ::: _ ] => f_equal | |

34 | [ |- hmap _ ?E = hmap _ ?E ] => f_equal | |

33 end; crush). | 35 end; crush). |

34 | 36 |

35 (** At this point in the book source, some auxiliary proofs also appear. *) | 37 (** At this point in the book source, some auxiliary proofs also appear. *) |

36 | 38 |

37 (* begin hide *) | 39 (* begin hide *) |