comparison src/Intro.v @ 563:af97676583f3

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 2a2a6a0241b5
children 81d63d9c1cc5
comparison
equal deleted inserted replaced
562:36b1f893c1e0 563:af97676583f3
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.4pl6, 8.5pl3, and 8.6. 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.6.1 and 8.7.1. 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