diff --git a/_CoqProject b/_CoqProject
index 271fa04fa6b711f142da368f52c03fac60319ae2..50b5c06cdde2b32c4b5735d1cea1f077f881eed5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6,6 +6,8 @@
 -arg -w -arg -convert_concl_no_check
 # non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
 -arg -w -arg -redundant-canonical-projection
+# "Declare Scope" does not exist yet in 8.9.
+-arg -w -arg -undeclared-scope
 # We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
 -arg -w -arg -ambiguous-paths
 
diff --git a/theories/logic/model.v b/theories/logic/model.v
index ffa2377b77b697a14ee8fcb05fe5415c823ade02..057ce90f36ee59cf9ea84e63bc85f16d2eda3c96 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -18,7 +18,6 @@ Record lrel Σ := LRel {
 }.
 Arguments LRel {_} _%I {_}.
 Arguments lrel_car {_} _ _ _ : simpl never.
-Declare Scope lrel_scope.
 Bind Scope lrel_scope with lrel.
 Delimit Scope lrel_scope with lrel.
 Existing Instance lrel_persistent.
diff --git a/theories/typing/types.v b/theories/typing/types.v
index d5722e9984748ca279dbbb1a313403f4d0a2ac13..ecc67ba81b00e8d81581c34e45e7b5384377b592 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -51,7 +51,6 @@ Fixpoint binop_bool_res_type (op : bin_op) : option type :=
   | _ => None
   end.
 
-Declare Scope FType_scope.
 Delimit Scope FType_scope with ty.
 Bind Scope FType_scope with type.
 Infix "*" := TProd : FType_scope.