comparison src/Intro.v @ 534:ed829eaa91b2

Builds with Coq 8.5beta2
author Adam Chlipala <adam@chlipala.net>
date Wed, 05 Aug 2015 14:46:55 -0400
parents 6b3fb6672cfa
children dac7a2705b00
comparison
equal deleted inserted replaced
533:8921cfa2f503 534:ed829eaa91b2
1 (* Copyright (c) 2008-2013, Adam Chlipala 1 (* Copyright (c) 2008-2013, 2015, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
184 *) 184 *)
185 185
186 (** ** Installation and Emacs Set-Up *) 186 (** ** Installation and Emacs Set-Up *)
187 187
188 (** 188 (**
189 At the start of the next chapter, I assume that you have installed Coq and Proof General. The code in this book is tested with Coq versions 8.4 and 8.4pl1. Though parts may work with other versions, it is expected that the book source will fail to build with _earlier_ versions. 189 At the start of the next chapter, I assume that you have installed Coq and Proof General. The code in this book is tested with Coq versions 8.4pl5 and 8.5beta2. Though parts may work with other versions, it is expected that the book source will fail to build with _earlier_ versions.
190 190
191 %\index{Proof General|(}%To set up your Proof General environment to process the source to the next chapter, a few simple steps are required. 191 %\index{Proof General|(}%To set up your Proof General environment to process the source to the next chapter, a few simple steps are required.
192 192
193 %\begin{enumerate}%#<ol># 193 %\begin{enumerate}%#<ol>#
194 194