diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 12599ed84672cd6ba41d89b6f223534841ccb180..424d2e16046daf8a970d59c21ce15204d0954856 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -53,13 +53,3 @@ build-coq.8.10.2:
   <<: *template
   variables:
     OPAM_PINS: "coq version 8.10.2"
-
-build-coq.8.9.1:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.9.1"
-
-build-coq.8.8.2:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.8.2"
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8152693b159cb34cceaf3c4383f9e218c4e81fb1..3bd27e03ff4745ffb4c29b024efc500be555c6cc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,8 @@ API-breaking change is listed.
 
 ## std++ master
 
+Coq 8.8 and 8.9 are no longer supported.
+
 - Rename `dom_map filter` → `dom_filter`, `dom_map_filter_L` → `dom_filter_L`,
   and `dom_map_filter_subseteq` → `dom_filter_subseteq` for consistency's sake.
 - Add `max` and `min` operations for `Qp`.
diff --git a/README.md b/README.md
index 329f151e832d88ea0b280949165f51e9154a50ed..4e218a7537cbf09535e277394acad694cec85e91 100644
--- a/README.md
+++ b/README.md
@@ -45,7 +45,7 @@ Notably:
 
 This version is known to compile with:
 
- - Coq version 8.8.2 / 8.9.1 / 8.10.2 / 8.11.2 / 8.12.0
+ - Coq version 8.10.2 / 8.11.2 / 8.12.0
 
 ## Installing via opam
 
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/coq-stdpp.opam b/coq-stdpp.opam
index aa072f1adc0b2b2658dfde3a351ca670d18e974d..f88d738648b851ff5ab75bf9e42542a38ab9064d 100644
--- a/coq-stdpp.opam
+++ b/coq-stdpp.opam
@@ -29,7 +29,7 @@ The key features of this library are as follows:
 """
 
 depends: [
-  "coq" { (= "8.8.2") | (>= "8.9.1" & < "8.13~") | (= "dev") }
+  "coq" { (>= "8.10.2" & < "8.13~") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
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/options.v b/theories/options.v
index c94b63dccfa6a69830312476090b40b948ebe1cb..7e3856858e2a8b84e9f61b0034e0de133151aee5 100644
--- a/theories/options.v
+++ b/theories/options.v
@@ -6,8 +6,7 @@ but not transitively. *)
 Export Set Default Proof Using "Type".
 (* FIXME: cannot enable this yet as some files disable 'Default Proof Using'.
 Export Set Suggest Proof Using. *)
-(* FIXME: cannot enable this on Coq 8.8.
-Export Set Default Goal Selector "!". *)
+Export Set Default Goal Selector "!".
 
 (* "Fake" import to whitelist this file for the check that ensures we import
 this file everywhere.
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.