diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 201dbd5f1322a01faaf3596460c7503aa42f72aa..c785411aa3a90f6be1d5139273af3306c7822046 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -54,7 +54,10 @@ stages:
     - "*/*/*/*/*/*/*/*/*/*.glob"
     expire_in: 1 week
 
-1.12.0-coq-8.13:
+1.13.0-coq-8.13:
+  extends: .build
+
+1.14.0-coq-8.13:
   extends: .build
 
 coq-8.13:
@@ -62,9 +65,3 @@ coq-8.13:
     - .build-dev
   # it's ok to fail with an unreleased version of ssreflect
   allow_failure: true
-
-coq-dev:
-  extends:
-    - .build-dev
-  # it's ok to fail with an unreleased version of ssreflect and Coq
-  allow_failure: true
diff --git a/mathcomp_complements.v b/mathcomp_complements.v
index ea214f5c3da6bf97446af9349941b598ea3e81b2..0afb04add5f7cde19f04aef178704cf0757ba905 100644
--- a/mathcomp_complements.v
+++ b/mathcomp_complements.v
@@ -1,7 +1,6 @@
-From mathcomp Require Import ssreflect ssrbool ssrfun fintype bigop
+From mathcomp Require Import ssreflect ssrbool ssrfun choice fintype bigop
      ssralg ssrnat order ssrnum rat.
-From mathcomp Require Import seq finfun path eqtype tuple.
-From mathcomp Require Import choice.
+From mathcomp Require Import seq finfun path eqtype tuple ssrint intdiv.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -9,8 +8,6 @@ Unset Printing Implicit Defensive.
 
 Import Order.Theory.
 
-From mathcomp Require Import div ssrint intdiv.
-
 Local Open Scope ring_scope.
 
 (* rat *)