pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-20 04:07:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Truly building with Coq 8.9 again

Browse source
This commit is contained in:
Adam Chlipala 2020-02-10 13:53:26 -05:00
parent 77f22213d8
commit 6ea006fccf
2 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
Interpreters.v
View file

@ -97,7 +97,8 @@ Proof.
equality. equality.
linear_arithmetic. rewrite IHe1, IHe2.
ring.
Qed. Qed.
(* Well, that's a relief! ;-) *) (* Well, that's a relief! ;-) *)

2
frap_book.tex
View file

@ -5461,7 +5461,7 @@ The project home page is:
\begin{center} \begin{center}
\url{https://coq.inria.fr/} \url{https://coq.inria.fr/}
\end{center} \end{center}
The code associated with this book is designed to work with Coq versions 8.10 and higher. The code associated with this book is designed to work with Coq versions 8.9 and higher.
The project Web site makes a number of versions available, and versions are also available in popular OS package distributions, along with binaries for platforms where open-source package systems are less common. The project Web site makes a number of versions available, and versions are also available in popular OS package distributions, along with binaries for platforms where open-source package systems are less common.
We assume that readers have installed Coq by one of those means or another. We assume that readers have installed Coq by one of those means or another.
It will also be almost essential to use some graphical interface for Coq editing. It will also be almost essential to use some graphical interface for Coq editing.