diff --git a/CompilerCorrectness.v b/CompilerCorrectness.v
index bf85744..c571e4b 100644
--- a/CompilerCorrectness.v
+++ b/CompilerCorrectness.v
@@ -40,7 +40,7 @@ Inductive cmd :=
 
 Coercion Const : nat >-> arith.
 Coercion Var : var >-> arith.
-Declare Scope arith_scope.
+(*Declare Scope arith_scope.*)
 Infix "+" := Plus : arith_scope.
 Infix "-" := Minus : arith_scope.
 Infix "*" := Times : arith_scope.
diff --git a/CompilerCorrectness_template.v b/CompilerCorrectness_template.v
index e357280..dcf571c 100644
--- a/CompilerCorrectness_template.v
+++ b/CompilerCorrectness_template.v
@@ -26,7 +26,7 @@ Inductive cmd :=
 
 Coercion Const : nat >-> arith.
 Coercion Var : var >-> arith.
-Declare Scope arith_scope.
+(*Declare Scope arith_scope.*)
 Infix "+" := Plus : arith_scope.
 Infix "-" := Minus : arith_scope.
 Infix "*" := Times : arith_scope.
diff --git a/FrapWithoutSets.v b/FrapWithoutSets.v
index fccc766..bd2ac72 100644
--- a/FrapWithoutSets.v
+++ b/FrapWithoutSets.v
@@ -101,7 +101,7 @@ Ltac instantiate_obviouses :=
 (** * Interlude: special notations and induction principle for [N] *)
 
 (* Note: recurse is an identifier, but we will always use the name "recurse" by convention *)
-Declare Scope N_recursion_scope.
+(*Declare Scope N_recursion_scope.*)
 Notation "recurse 'by' 'cases' | 0 => A | n + 1 => B 'end'" :=
   (N.recursion A (fun n recurse => B))
   (at level 11, A at level 200, n at level 0, B at level 200,
diff --git a/HoareLogic.v b/HoareLogic.v
index e2ab5fd..2ddf399 100644
--- a/HoareLogic.v
+++ b/HoareLogic.v
@@ -170,7 +170,7 @@ Qed.
 (* BEGIN syntax macros that won't be explained *)
 Coercion Const : nat >-> exp.
 Coercion Var : string >-> exp.
-Declare Scope cmd_scope.
+(*Declare Scope cmd_scope.*)
 Notation "*[ e ]" := (Read e) : cmd_scope.
 Infix "+" := Plus : cmd_scope.
 Infix "-" := Minus : cmd_scope.
@@ -190,7 +190,7 @@ Notation "{{ I }} 'while' b 'loop' body 'done'" := (While_ I b body) (at level 7
 Notation "'assert' {{ I }}" := (Assert I) (at level 75).
 Delimit Scope cmd_scope with cmd.
 
-Declare Scope reset_scope.
+(*Declare Scope reset_scope.*)
 Infix "+" := plus : reset_scope.
 Infix "-" := Init.Nat.sub : reset_scope.
 Infix "*" := mult : reset_scope.
diff --git a/Imp.v b/Imp.v
index e349a8a..aec61ee 100644
--- a/Imp.v
+++ b/Imp.v
@@ -19,7 +19,7 @@ Inductive cmd :=
 
 Coercion Const : nat >-> arith.
 Coercion Var : var >-> arith.
-Declare Scope arith_scope.
+(*Declare Scope arith_scope.*)
 Infix "+" := Plus : arith_scope.
 Infix "-" := Minus : arith_scope.
 Infix "*" := Times : arith_scope.
diff --git a/Interpreters.v b/Interpreters.v
index 50b7a85..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! ;-) *)
 
@@ -309,7 +310,7 @@ Example factorial_ugly :=
  * them from our examples. *)
 Coercion Const : nat >-> arith.
 Coercion Var : var >-> arith.
-Declare Scope arith_scope.
+(*Declare Scope arith_scope.*)
 Infix "+" := Plus : arith_scope.
 Infix "-" := Minus : arith_scope.
 Infix "*" := Times : arith_scope.
diff --git a/Interpreters_template.v b/Interpreters_template.v
index d289bf9..bfb4b05 100644
--- a/Interpreters_template.v
+++ b/Interpreters_template.v
@@ -249,7 +249,7 @@ Example factorial_ugly :=
  * them from our examples. *)
 Coercion Const : nat >-> arith.
 Coercion Var : var >-> arith.
-Declare Scope arith_scope.
+(*Declare Scope arith_scope.*)
 Infix "+" := Plus : arith_scope.
 Infix "-" := Minus : arith_scope.
 Infix "*" := Times : arith_scope.
diff --git a/Polymorphism.v b/Polymorphism.v
index 287acba..659de38 100644
--- a/Polymorphism.v
+++ b/Polymorphism.v
@@ -448,7 +448,7 @@ Inductive statement : Set :=
  * almost-natural-looking embedded programs in Coq. *)
 Coercion Const : nat >-> expression.
 Coercion Var : string >-> expression.
-Declare Scope embedded_scope.
+(*Declare Scope embedded_scope.*)
 Infix "+" := Plus : embedded_scope.
 Infix "-" := Minus : embedded_scope.
 Infix "*" := Times : embedded_scope.
diff --git a/Polymorphism_template.v b/Polymorphism_template.v
index 2beb84b..9414ccc 100644
--- a/Polymorphism_template.v
+++ b/Polymorphism_template.v
@@ -291,7 +291,7 @@ Inductive statement : Set :=
  * almost-natural-looking embedded programs in Coq. *)
 Coercion Const : nat >-> expression.
 Coercion Var : string >-> expression.
-Declare Scope embedded_scope.
+(*Declare Scope embedded_scope.*)
 Infix "+" := Plus : embedded_scope.
 Infix "-" := Minus : embedded_scope.
 Infix "*" := Times : embedded_scope.
diff --git a/_CoqProject b/_CoqProject
index 19d5cab..6b3e8f6 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,4 +1,5 @@
 -R . Frap
+-arg -w -arg -undeclared-scope
 Map.v
 Var.v
 Sets.v
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.