diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 63137a3dae1f76286a02d8b9d89a341ffa1e229c..1fa75c28797a6a1f7544030ae2f3c606c272fcea 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -43,7 +43,7 @@ opam:
 build-coq.8.7.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.7.dev   coq-mathcomp-ssreflect version dev"
+    OPAM_PINS: "coq version 8.7.dev"
   artifacts:
     paths:
     - build-time.txt
diff --git a/opam b/opam
index 2f9b1ff1163fc8a3ac98a64167694766735b0095..84f0313fbd3631c85da14a46ed4da0a41df95414 100644
--- a/opam
+++ b/opam
@@ -10,7 +10,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
-  "coq" { >= "8.6.1" & < "8.8~" }
-  "coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
+  "coq" { >= "8.7.0" & < "8.8~" }
   "coq-stdpp" { (= "dev.2017-11-12.2") | (= "dev") }
 ]
diff --git a/theories/algebra/base.v b/theories/algebra/base.v
index 79f8e4978406798c1221ae3887e41e39da0d2565..603e9c20cebe850070a8c639514fcc2949b87a97 100644
--- a/theories/algebra/base.v
+++ b/theories/algebra/base.v
@@ -1,8 +1,6 @@
-From mathcomp Require Export ssreflect.
+From Coq.ssr Require Export ssreflect.
 From stdpp Require Export prelude.
 Set Default Proof Using "Type".
-(* Reset options set by the ssreflect plugin to their defaults *)
-Global Set Bullet Behavior "Strict Subproofs".
 Global Open Scope general_if_scope.
-Global Unset Asymmetric Patterns.
+Global Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
 Ltac done := stdpp.tactics.done.