diff --git a/_CoqProject b/_CoqProject
index a90e9b51ecef2f8a9c7b7e00b91f9ec8950e68e3..77e45b94de9eec153fba2fe35d973172793159ac 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,6 +1,4 @@
 -Q theories stdpp
-# "Declare Scope" does not exist yet in 8.9.
--arg -w -arg -undeclared-scope
 
 theories/options.v
 theories/base.v
diff --git a/theories/base.v b/theories/base.v
index 603fe11a829333a84def3835562361a7a752ebe0..ceb16eef8fd3778c65375b35311ffbf83b3026f1 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -183,6 +183,7 @@ Definition tc_to_bool (P : Prop)
 
 (** Throughout this development we use [stdpp_scope] for all general purpose
 notations that do not belong to a more specific scope. *)
+Declare Scope stdpp_scope.
 Delimit Scope stdpp_scope with stdpp.
 Global Open Scope stdpp_scope.
 
diff --git a/theories/binders.v b/theories/binders.v
index ce03ccd9a3ce67eb1df80d0a95557ff9a8e156d3..b2d2f4f942e3144f0eb49e615294535dbd0e901f 100644
--- a/theories/binders.v
+++ b/theories/binders.v
@@ -12,9 +12,11 @@ From stdpp Require Import options.
 (* Pick up extra assumptions from section parameters. *)
 Set Default Proof Using "Type*".
 
+Declare Scope binder_scope.
+Delimit Scope binder_scope with binder.
+
 Inductive binder := BAnon | BNamed :> string → binder.
 Bind Scope binder_scope with binder.
-Delimit Scope binder_scope with binder.
 Notation "<>" := BAnon : binder_scope.
 
 Instance binder_dec_eq : EqDecision binder.
diff --git a/theories/fin.v b/theories/fin.v
index dc99e703ef37af27505fc37ff958b81f15126945..5e72506bdddbc90d7801c85fea7d84cf0f2488ae 100644
--- a/theories/fin.v
+++ b/theories/fin.v
@@ -15,6 +15,7 @@ ambiguity. *)
 Notation fin := Fin.t.
 Notation FS := Fin.FS.
 
+Declare Scope fin_scope.
 Delimit Scope fin_scope with fin.
 Arguments Fin.FS _ _%fin : assert.
 
diff --git a/theories/numbers.v b/theories/numbers.v
index 3976a72bfe94d659e48956945bf9d166cf48760d..420c82d4870eb717d4ec36701339f88c1e7bcecf 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -658,13 +658,15 @@ Qed.
 Local Close Scope Qc_scope.
 
 (** * Positive rationals *)
+Declare Scope Qp_scope.
+Delimit Scope Qp_scope with Qp.
+
 (** The theory of positive rationals is very incomplete. We merely provide
 some operations and theorems that are relevant for fractional permissions. *)
 Record Qp := mk_Qp { Qp_car :> Qc ; Qp_prf : (0 < Qp_car)%Qc }.
 Hint Resolve Qp_prf : core.
-Delimit Scope Qp_scope with Qp.
-Bind Scope Qp_scope with Qp.
 Arguments Qp_car _%Qp : assert.
+Bind Scope Qp_scope with Qp.
 
 Local Open Scope Qc_scope.
 Local Open Scope Qp_scope.
diff --git a/theories/streams.v b/theories/streams.v
index 7022bfba05ea262e5ec78b742fca3d24aae0384f..50c219c85d0b751459afbd4a124428eea21d131c 100644
--- a/theories/streams.v
+++ b/theories/streams.v
@@ -1,12 +1,14 @@
 From stdpp Require Export tactics.
 From stdpp Require Import options.
 
-CoInductive stream (A : Type) : Type := scons : A → stream A → stream A.
-Arguments scons {_} _ _ : assert.
+Declare Scope stream_scope.
 Delimit Scope stream_scope with stream.
-Bind Scope stream_scope with stream.
 Open Scope stream_scope.
+
+CoInductive stream (A : Type) : Type := scons : A → stream A → stream A.
+Arguments scons {_} _ _ : assert.
 Infix ":.:" := scons (at level 60, right associativity) : stream_scope.
+Bind Scope stream_scope with stream.
 
 Definition shead {A} (s : stream A) : A := match s with x :.: _ => x end.
 Definition stail {A} (s : stream A) : stream A := match s with _ :.: s => s end.