aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorCyril Cohen2021-03-07 12:58:22 +0100
committerGitHub2021-03-07 12:58:22 +0100
commit573fa17081935f637e500a945eefa289d3361f1c (patch)
tree85fcc9c1dad0e216dde51de8268f26bd3d08008c
parent2b61b2b69892fa0eccf2d3f2ecd408c25731b578 (diff)
mathcomp analysis does not compire with Coq dev for now
-rw-r--r--.gitlab-ci.yml5
1 files changed, 0 insertions, 5 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 8a5c7f0..0b3de75 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -432,11 +432,6 @@ ci-analysis-8.13:
variables:
COQ_VERSION: "8.13"
-ci-analysis-dev:
- extends: .ci-analysis
- variables:
- COQ_VERSION: "dev"
-
# The FCSL-PCM library
.ci-fcsl-pcm:
extends: .ci