Mercurial > cpdt > repo

diff src/Universes.v @ 563:af97676583f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update for extraction to work in Coq 8.7, which unfortunately at last breaks compatibility with Coq versions before 8.6
author Adam Chlipala <adam@chlipala.net>
date Sun, 07 Jan 2018 11:53:31 -0500
parents 2c8c693ddaba
children 81d63d9c1cc5
line wrap: on
line diff
--- a/src/Universes.v	Mon Dec 18 17:05:53 2017 -0500
+++ b/src/Universes.v	Sun Jan 07 11:53:31 2018 -0500
@@ -12,6 +12,8 @@
 
 Require Import DepList Cpdt.CpdtTactics.
 
+Require Extraction.
+
 Set Implicit Arguments.
 Set Asymmetric Patterns.
 (* end hide *)
@@ -1070,7 +1072,7 @@
 
   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. *)
+                     * 8.4 and 8.5. *)
 (** %\vspace{-.15in}%[[
   H : proof p
   H1 : And p q = And p0 q0