diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index e326bbffba2863fe8fb99094a892c385c7eaa63a..1de5533e8c2c9a0898bf0b4de78e19db0c455913 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -78,12 +78,3 @@ build-coq.8.7.0:
   variables:
     OPAM_PINS: "coq version 8.7.0"
 
-build-coq.8.6.1:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.6.1"
-
-build-coq.8.6.0:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.6"
diff --git a/README.md b/README.md
index 2dbdd6719eba7b6cb1a313f9a451f38c1d9982dd..54b646278b111da17c1cf6d15e8f86da72c58f99 100644
--- a/README.md
+++ b/README.md
@@ -33,19 +33,19 @@ Notably:
 * The behavior of `Program` is tweaked: `Unset Transparent Obligations`,
   `Obligation Tactic := idtac`, `Add Search Blacklist "_obligation_"`.  See
   [`base.v`](theories/base.v) for further details.
-* It blocks `simpl` on all operations on integers `Z` (by setting
+* It blocks `simpl` on all operations involving integers `Z` (by setting
   `Arguments op : simpl never`). We do this because `simpl` tends to expose
-  their internals (e.g. try `simpl` on `Z.of_nat (S n) + y`).
+  the internals of said operations (e.g. try `simpl` on `Z.of_nat (S n) + y`).
   As a consequence of blocking `simpl`, due to
   [Coq bug #5039](https://github.com/coq/coq/issues/5039) the `omega` tactic
-  sometimes fails. We do not consider this an issue since we use `lia` (for
-  which the aforementioned Coq bug was fixed) instead of `omega` anywhere.
+  becomes unreliable. We do not consider this an issue since we use `lia` (for
+  which the aforementioned Coq bug was fixed) instead of `omega` everywhere.
 
 ## Prerequisites
 
 This version is known to compile with:
 
- - Coq version 8.6.0 / 8.6.1 / 8.7.0 / 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1 / 8.8.2
+ - Coq version 8.7.0 / 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1 / 8.8.2
 
 ## Installing via opam
 
diff --git a/opam b/opam
index a53b161925660e812d8dc3b196da9715ca989d9d..a12aba6335c8c85ab180c2d84859452982b09920 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/stdpp"]
 depends: [
-  "coq" { (>= "8.6" & < "8.10~") | (= "dev") }
+  "coq" { (>= "8.7" & < "8.10~") | (= "dev") }
 ]