1 files changed, 87 insertions, 31 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 52ff725..1bb8aca 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -324,37 +324,36 @@ ci-bigenough-dev:
   variables:
     COQ_VERSION: "dev"
 
-# # The real-closed library
-# .ci-real-closed:
-#   extends: .ci
-#   variables:
-#     CONTRIB_URL: "https://github.com/math-comp/real-closed.git"
-#     CONTRIB_VERSION: master
-#   script:
-#     - opam pin add -n -k path coq-mathcomp-real-closed .
-#     - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-real-closed
-#     - opam install -y -v -j "${NJOBS}" coq-mathcomp-real-closed
-# 
-# ci-real-closed-dev:
-#   extends: .ci-real-closed
-#   variables:
-#     COQ_VERSION: "dev"
-# 
-# # The analysis library
-# .ci-analysis:
-#   extends: .ci
-#   variables:
-#     CONTRIB_URL: "https://github.com/math-comp/analysis.git"
-#     CONTRIB_VERSION: master
-#   script:
-#     - opam pin add -n -k path coq-mathcomp-analysis .
-#     - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-analysis
-#     - opam install -y -v -j "${NJOBS}" coq-mathcomp-analysis
-# 
-# ci-analysis-dev:
-#   extends: .ci-analysis
-#   variables:
-#     COQ_VERSION: "dev"
+# The real-closed library
+.ci-real-closed:
+  extends: .ci
+  variables:
+    CONTRIB_URL: "https://github.com/math-comp/real-closed.git"
+    CONTRIB_VERSION: master
+  script:
+    - opam pin add -n -k path coq-mathcomp-real-closed .
+    - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-real-closed
+    - opam install -y -v -j "${NJOBS}" coq-mathcomp-real-closed
+
+ci-real-closed-8.10:
+  extends: .ci-real-closed
+  variables:
+    COQ_VERSION: "8.10"
+
+ci-real-closed-8.11:
+  extends: .ci-real-closed
+  variables:
+    COQ_VERSION: "8.11"
+
+ci-real-closed-8.12:
+  extends: .ci-real-closed
+  variables:
+    COQ_VERSION: "8.12"
+
+ci-real-closed-dev:
+  extends: .ci-real-closed
+  variables:
+    COQ_VERSION: "dev"
 
 # The finmap library
 .ci-finmap:
@@ -387,6 +386,63 @@ ci-finmap-dev:
   variables:
     COQ_VERSION: "dev"
 
+# The multinomials library
+.ci-multinomials:
+  extends: .ci
+  variables:
+    CONTRIB_URL: "https://github.com/math-comp/multinomials.git"
+    CONTRIB_VERSION: master
+  script:
+    - opam pin add -n -k path coq-mathcomp-multinomials .
+    - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-multinomials
+    - opam install -y -v -j "${NJOBS}" coq-mathcomp-multinomials
+
+ci-multinomials-8.10:
+  extends: .ci-multinomials
+  variables:
+    COQ_VERSION: "8.10"
+
+ci-multinomials-8.11:
+  extends: .ci-multinomials
+  variables:
+    COQ_VERSION: "8.11"
+
+ci-multinomials-8.12:
+  extends: .ci-multinomials
+  variables:
+    COQ_VERSION: "8.12"
+
+ci-multinomials-dev:
+  extends: .ci-multinomials
+  variables:
+    COQ_VERSION: "dev"
+
+# The analysis library
+.ci-analysis:
+  extends: .ci
+  variables:
+    CONTRIB_URL: "https://github.com/math-comp/analysis.git"
+    CONTRIB_VERSION: master
+  script:
+    - opam pin add -n -k path coq-mathcomp-analysis .
+    - opam install -y -v -j "${NJOBS}" --deps-only coq-mathcomp-analysis
+    - opam install -y -v -j "${NJOBS}" coq-mathcomp-analysis
+
+ci-analysis-8.11:
+  extends: .ci-analysis
+  variables:
+    COQ_VERSION: "8.11"
+
+ci-analysis-8.12:
+  extends: .ci-analysis
+  variables:
+    COQ_VERSION: "8.12"
+
+ci-analysis-dev:
+  extends: .ci-analysis
+  variables:
+    COQ_VERSION: "dev"
+
 # The FCSL-PCM library
 .ci-fcsl-pcm:
   extends: .ci