Mercurial > cpdt > repo

comparison 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
comparison
equal deleted inserted replaced
546:306539f29eea 547:2c8c693ddaba
1066 proof p 1066 proof p
1067 ]] 1067 ]]
1068 1068
1069 The first goal looks reasonable. Hypothesis [H0] is clearly contradictory, as [discriminate] can show. *) 1069 The first goal looks reasonable. Hypothesis [H0] is clearly contradictory, as [discriminate] can show. *)
1070 1070
1071 discriminate. 1071 try discriminate. (* Note: Coq 8.6 is now solving this subgoal automatically!
1072 * This line left here to keep everything working in
1073 * 8.4, 8.5, and 8.6. *)
1072 (** %\vspace{-.15in}%[[ 1074 (** %\vspace{-.15in}%[[
1073 H : proof p 1075 H : proof p
1074 H1 : And p q = And p0 q0 1076 H1 : And p q = And p0 q0
1075 ============================ 1077 ============================
1076 proof p0 1078 proof p0