Mercurial > cpdt > repo
diff 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 |
line wrap: on
line diff
--- a/src/Intro.v Mon Dec 18 17:05:53 2017 -0500 +++ b/src/Intro.v Sun Jan 07 11:53:31 2018 -0500 @@ -186,7 +186,7 @@ (** ** Installation and Emacs Set-Up *) (** -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. +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. %\index{Proof General|(}%To set up your Proof General environment to process the source to the next chapter, a few simple steps are required.