Mercurial > cpdt > repo

diff src/Universes.v @ 554:93471096cdd4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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