5 files changed, 14 insertions, 50 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 10b4f9b044..98ea594366 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -16,12 +16,9 @@ We are currently running tests on the following platforms:
   `./configure`. It should allow complying with this discipline
   without pain.
 
-- AppVeyor is used to test the compilation of Coq and run the test-suite on
-  Windows.
-
 - Azure Pipelines is used to test the compilation of Coq and run the
-  test-suite on Windows and on macOS. It is expected to replace
-  appveyor eventually.
+  test-suite on Windows and on macOS. It is expected to be used to build
+  macOS and Windows packages eventually.
 
 You can anticipate the results of most of these tests prior to submitting your
 PR by running GitLab CI on your private branches. To do so follow these steps:
diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat
deleted file mode 100644
index 341b875edc..0000000000
--- a/dev/ci/appveyor.bat
+++ /dev/null
@@ -1,42 +0,0 @@
-REM This script either runs the test suite with OPAM (if USEOPAM is true) or
-REM builds the Coq binary packages for windows (if USEOPAM is false).
-
-if %ARCH% == 32 (
-  SET ARCHLONG=i686
-  SET CYGROOT=C:\cygwin
-  SET SETUP=setup-x86.exe
-)
-
-if %ARCH% == 64 (
-  SET ARCHLONG=x86_64
-  SET CYGROOT=C:\cygwin64
-  SET SETUP=setup-x86_64.exe
-)
-
-SET CYGCACHE=%CYGROOT%\var\cache\setup
-SET APPVEYOR_BUILD_FOLDER_MFMT=%APPVEYOR_BUILD_FOLDER:\=/%
-SET APPVEYOR_BUILD_FOLDER_CFMT=%APPVEYOR_BUILD_FOLDER_MFMT:C:/=/cygdrive/c/%
-SET DESTCOQ=C:\coq%ARCH%_inst
-SET COQREGTESTING=Y
-
-if %USEOPAM% == false (
-  call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
-    -arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^
-    -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
-    -addon=bignums -make=N ^
-    -setup %CYGROOT%\%SETUP% || GOTO ErrorExit
-  copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit
-  7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
-)
-
-if %USEOPAM% == true (
-  %CYGROOT%\%SETUP% -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% ^
-    -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time
-  %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh || GOTO ErrorExit
-)
-
-GOTO :EOF
-
-:ErrorExit
-  ECHO ERROR %0 failed
-  EXIT /b 1
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 8dee465cf4..74e8d3bbaa 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -35,7 +35,7 @@
 : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}"
 : "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}"
 
-: "${mtac2_CI_REF:=master-sync}"
+: "${mtac2_CI_REF:=master}"
 : "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2}"
 : "${mtac2_CI_ARCHIVEURL:=${mtac2_CI_GITURL}/archive}"
 
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index baf470e021..4cd7faf757 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-12-14-V1"
+# CACHEKEY: "bionic_coq-V2019-01-28-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -38,7 +38,7 @@ ENV COMPILER="4.05.0"
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
 ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.3.0" \
-    CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
+    CI_OPAM="menhir.20181113 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
diff --git a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh b/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh
new file mode 100644
index 0000000000..6e89741e29
--- /dev/null
+++ b/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "6914" ] || [ "$CI_BRANCH" = "primitive-bool-list" ]; then
+
+    bignums_CI_REF=primitive-integers
+    bignums_CI_GITURL=https://github.com/vbgl/bignums
+
+    mtac2_CI_REF=primitive-integers
+    mtac2_CI_GITURL=https://github.com/vbgl/Mtac2
+
+fi