## Mercurial > cpdt > repo

### comparison src/Universes.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 | af97676583f3 |

comparison

equal
deleted
inserted
replaced

546:306539f29eea | 547:2c8c693ddaba |
---|---|

1066 proof p | 1066 proof p |

1067 ]] | 1067 ]] |

1068 | 1068 |

1069 The first goal looks reasonable. Hypothesis [H0] is clearly contradictory, as [discriminate] can show. *) | 1069 The first goal looks reasonable. Hypothesis [H0] is clearly contradictory, as [discriminate] can show. *) |

1070 | 1070 |

1071 discriminate. | 1071 try discriminate. (* Note: Coq 8.6 is now solving this subgoal automatically! |

1072 * This line left here to keep everything working in | |

1073 * 8.4, 8.5, and 8.6. *) | |

1072 (** %\vspace{-.15in}%[[ | 1074 (** %\vspace{-.15in}%[[ |

1073 H : proof p | 1075 H : proof p |

1074 H1 : And p q = And p0 q0 | 1076 H1 : And p q = And p0 q0 |

1075 ============================ | 1077 ============================ |

1076 proof p0 | 1078 proof p0 |