Avoid a command only introduced in Coq 8.10, so that 8.9 keeps working

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.

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.

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,

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.

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.

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.

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.

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.

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.

_CoqProject

@@ -1,4 +1,5 @@
 -R . Frap
+-arg -w -arg -undeclared-scope
 Map.v
 Var.v
 Sets.v