From 0c49f8c4c03659126e7976390fc6ec876fd6c1ce Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 25 Nov 2020 15:44:55 +0100
Subject: [ci] coquelicot, depend on ssr proper

---
 .gitlab-ci.yml          | 11 +++++++++--
 Makefile.ci             |  2 +-
 dev/ci/ci-coquelicot.sh |  2 --
 3 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 9fb0fc581c..a37641fba9 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -738,7 +738,14 @@ library:ci-coqtail:
   extends: .ci-template
 
 library:ci-coquelicot:
-  extends: .ci-template
+  stage: stage-3
+  extends: .ci-template-flambda
+  needs:
+  - build:edge+flambda
+  - library:ci-mathcomp
+  dependencies:
+  - build:edge+flambda
+  - library:ci-mathcomp
 
 library:ci-cross_crypto:
   extends: .ci-template
@@ -794,7 +801,7 @@ library:ci-menhir:
 
 library:ci-interval:
   extends: .ci-template-flambda
-  stage: stage-3
+  stage: stage-4
   needs:
   - build:edge+flambda
   - library:ci-coquelicot
diff --git a/Makefile.ci b/Makefile.ci
index fd41884e5c..9f08de662f 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -72,7 +72,7 @@ ci-all: $(CI_TARGETS)
 ci-color: ci-bignums
 
 ci-coqprime: ci-bignums
-
+ci-coquelicot: ci-mathcomp
 ci-math_classes: ci-bignums
 
 ci-corn: ci-math_classes
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index 5b4d953e7b..777d36a6d7 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-install_ssreflect
-
 git_download coquelicot
 
 ( cd "${CI_BUILD_DIR}/coquelicot" && ( if [ ! -x ./configure ]; then autoreconf -i -s && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install )
-- 
cgit v1.2.3