From 6ea006fccf265fed587d23487433137efa51066c Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Mon, 10 Feb 2020 13:53:26 -0500 Subject: [PATCH] Truly building with Coq 8.9 again --- Interpreters.v | 3 ++- frap_book.tex | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Interpreters.v b/Interpreters.v index 1f09506..e06d7ed 100644 --- a/Interpreters.v +++ b/Interpreters.v @@ -97,7 +97,8 @@ Proof. equality. - linear_arithmetic. + rewrite IHe1, IHe2. + ring. Qed. (* Well, that's a relief! ;-) *) diff --git a/frap_book.tex b/frap_book.tex index a96a196..846bf71 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -5461,7 +5461,7 @@ The project home page is: \begin{center} \url{https://coq.inria.fr/} \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. 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.