Mercurial > cpdt > repo
diff src/Universes.v @ 554:93471096cdd4
Merge
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sat, 19 Aug 2017 12:14:40 -0400 |
parents | 2c8c693ddaba |
children | af97676583f3 |
line wrap: on
line diff
--- a/src/Universes.v Sat Aug 19 12:14:26 2017 -0400 +++ b/src/Universes.v Sat Aug 19 12:14:40 2017 -0400 @@ -1068,7 +1068,9 @@ The first goal looks reasonable. Hypothesis [H0] is clearly contradictory, as [discriminate] can show. *) - discriminate. + try discriminate. (* Note: Coq 8.6 is now solving this subgoal automatically! + * This line left here to keep everything working in + * 8.4, 8.5, and 8.6. *) (** %\vspace{-.15in}%[[ H : proof p H1 : And p q = And p0 q0