Mercurial > cpdt > repo

diff 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
line wrap: on
line diff
--- a/src/Universes.v	Thu May 12 18:09:36 2016 -0500
+++ b/src/Universes.v	Wed Jul 12 13:08:24 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