Use the version of ssreflect that's shipped with Coq 8.7.

.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

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") }
 ]

theories/algebra/base.v

-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.