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..1f09506 100644
--- a/Interpreters.v
+++ b/Interpreters.v
@@ -309,7 +309,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