diff --git a/.travis.yml b/.travis.yml
index 9f4fe1e..f2f2c86 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -42,21 +42,15 @@ matrix:
   - env:
     - COQ=8.10
     <<: *NIX
-  - env:
-    - COQ=8.9
-    <<: *NIX
-  - env:
-    - COQ=8.8
-    <<: *NIX
 
   # Test supported versions of Coq via OPAM
   - env:
-    - COQ_IMAGE=coqorg/coq:dev
+    - COQ_IMAGE=coqorg/coq:8.11
     - PACKAGE=coq-lemma-overloading.dev
     - NJOBS=2
     <<: *OPAM
   - env:
-    - COQ_IMAGE=coqorg/coq:8.11
+    - COQ_IMAGE=coqorg/coq:dev
     - PACKAGE=coq-lemma-overloading.dev
     - NJOBS=2
     <<: *OPAM
diff --git a/README.md b/README.md
index 8af155f..b58d296 100644
--- a/README.md
+++ b/README.md
@@ -45,8 +45,8 @@ re-implementations for comparison.
   - Anton Trunov ([**@anton-trunov**](https://github.com/anton-trunov))
   - Karl Palmskog ([**@palmskog**](https://github.com/palmskog))
 - License: [GNU General Public License v3.0 or later](LICENSE.md)
-- Compatible Coq versions: 8.8 or later (use releases for other Coq versions)
-- Additional Coq dependencies:
+- Compatible Coq versions: 8.10 or later (use releases for other Coq versions)
+- Additional dependencies:
   - [MathComp](https://math-comp.github.io) 1.7.0 or later (`ssreflect` suffices)
 - Coq namespace: `LemmaOverloading`
 - Related publication(s):
diff --git a/_CoqProject b/_CoqProject
index 2d8713a..bcda722 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,7 +4,6 @@
 -arg -w -arg -notation-overridden
 -arg -w -arg -projection-no-head-constant
 -arg -w -arg -redundant-canonical-projection
--arg -w -arg -undeclared-scope
 
 theories/prelude.v
 theories/rels.v
diff --git a/coq-lemma-overloading.opam b/coq-lemma-overloading.opam
index 22c58df..56f14c7 100644
--- a/coq-lemma-overloading.opam
+++ b/coq-lemma-overloading.opam
@@ -22,8 +22,7 @@ re-implementations for comparison."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "ocaml"
-  "coq" {(>= "8.8" & < "8.12~") | (= "dev")}
+  "coq" {(>= "8.10" & < "8.12~") | (= "dev")}
   "coq-mathcomp-ssreflect" {(>= "1.7" & < "1.11~") | (= "dev")}
 ]
 
diff --git a/meta.yml b/meta.yml
index 32ad506..3c7afac 100644
--- a/meta.yml
+++ b/meta.yml
@@ -55,17 +55,15 @@ license:
   file: LICENSE.md
 
 supported_coq_versions:
-  text: 8.8 or later (use releases for other Coq versions)
-  opam: '{(>= "8.8" & < "8.12~") | (= "dev")}'
+  text: 8.10 or later (use releases for other Coq versions)
+  opam: '{(>= "8.10" & < "8.12~") | (= "dev")}'
 
 tested_coq_nix_versions:
 - version_or_url: '8.10'
-- version_or_url: '8.9'
-- version_or_url: '8.8'
 
 tested_coq_opam_versions:
-- version: dev
 - version: '8.11'
+- version: dev
 
 dependencies:
 - opam:
diff --git a/theories/rels.v b/theories/rels.v
index b54fb6d..2eb4b90 100644
--- a/theories/rels.v
+++ b/theories/rels.v
@@ -34,6 +34,7 @@ Lemma orpT p : p \/ True <-> True.    Proof. by intuition. Qed.
 Lemma orFp p : False \/ p <-> p.      Proof. by intuition. Qed.
 Lemma orpF p : p \/ False <-> p.      Proof. by intuition. Qed.
 
+Declare Scope rel_scope.
 Delimit Scope rel_scope with rel.
 Open Scope rel_scope.
 
diff --git a/theories/stsep.v b/theories/stsep.v
index 0a9bf2b..2d6f9b9 100644
--- a/theories/stsep.v
+++ b/theories/stsep.v
@@ -23,6 +23,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Declare Scope stsep_scope.
 Delimit Scope stsep_scope with stsep.
 Open Scope stsep_scope.