From ff6d9982d940702e413a29e09baf4ba3b00e4ccc Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre@roux01.fr>
Date: Tue, 22 Feb 2022 10:32:23 +0100
Subject: [PATCH] Update gitlab CI
---
.gitlab-ci.yml | 11 ++++-------
mathcomp_complements.v | 7 ++-----
2 files changed, 6 insertions(+), 12 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 201dbd5f..c785411a 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 ea214f5c..0afb04ad 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 *)
--
GitLab