Mercurial > cpdt > repo

comparison 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
comparison
equal deleted inserted replaced
562:36b1f893c1e0 563:af97676583f3
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import List. 11 Require Import List.
12 12
13 Require Import DepList Cpdt.CpdtTactics. 13 Require Import DepList Cpdt.CpdtTactics.
14
15 Require Extraction.
14 16
15 Set Implicit Arguments. 17 Set Implicit Arguments.
16 Set Asymmetric Patterns. 18 Set Asymmetric Patterns.
17 (* end hide *) 19 (* end hide *)
18 20
1068 1070
1069 The first goal looks reasonable. Hypothesis [H0] is clearly contradictory, as [discriminate] can show. *) 1071 The first goal looks reasonable. Hypothesis [H0] is clearly contradictory, as [discriminate] can show. *)
1070 1072
1071 try discriminate. (* Note: Coq 8.6 is now solving this subgoal automatically! 1073 try discriminate. (* Note: Coq 8.6 is now solving this subgoal automatically!
1072 * This line left here to keep everything working in 1074 * This line left here to keep everything working in
1073 * 8.4, 8.5, and 8.6. *) 1075 * 8.4 and 8.5. *)
1074 (** %\vspace{-.15in}%[[ 1076 (** %\vspace{-.15in}%[[
1075 H : proof p 1077 H : proof p
1076 H1 : And p q = And p0 q0 1078 H1 : And p q = And p0 q0
1077 ============================ 1079 ============================
1078 proof p0 1080 proof p0