32 files changed, 193 insertions, 127 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 6663fbecf8..98ea594366 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -16,14 +16,9 @@ We are currently running tests on the following platforms:
   `./configure`. It should allow complying with this discipline
   without pain.
 
-- Travis CI is used to test the compilation of Coq and run the test-suite on
-  macOS.
-
-- 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. 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/appveyor.sh b/dev/ci/appveyor.sh
index 470d07b27d..f26e0904bc 100644
--- a/dev/ci/appveyor.sh
+++ b/dev/ci/appveyor.sh
@@ -3,14 +3,15 @@
 set -e -x
 
 APPVEYOR_OPAM_VARIANT=ocaml-variants.4.07.1+mingw64c
+NJOBS=2
 
 wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz
 tar -xf opam64.tar.xz
 bash opam64/install.sh
 
-opam init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $APPVEYOR_OPAM_VARIANT --disable-sandboxing
+opam init default -j $NJOBS -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $APPVEYOR_OPAM_VARIANT --disable-sandboxing
 eval "$(opam env)"
-opam install -y num ocamlfind ounit
+opam install -j $NJOBS -y num ocamlfind ounit
 
 # Full regular Coq Build
-cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte # && make -C test-suite all INTERACTIVE= # && make validate
+cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make -j $NJOBS && make byte -j $NJOBS && make -j $NJOBS -C test-suite all INTERACTIVE= # && make validate
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/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh
index 5205946261..2ac78d3c2b 100755
--- a/dev/ci/ci-bedrock2.sh
+++ b/dev/ci/ci-bedrock2.sh
@@ -6,4 +6,4 @@ ci_dir="$(dirname "$0")"
 FORCE_GIT=1
 git_download bedrock2
 
-( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && make )
+( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && COQMF_ARGS='-arg "-async-proofs-tac-j 1"' make )
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index a5aa54144c..b4d2a9ca4e 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -62,27 +62,30 @@ git_download()
 {
   local PROJECT=$1
   local DEST="$CI_BUILD_DIR/$PROJECT"
+  local GITURL_VAR="${PROJECT}_CI_GITURL"
+  local GITURL="${!GITURL_VAR}"
+  local REF_VAR="${PROJECT}_CI_REF"
+  local REF="${!REF_VAR}"
 
   if [ -d "$DEST" ]; then
     echo "Warning: download and unpacking of $PROJECT skipped because $DEST already exists."
   elif [ "$FORCE_GIT" = "1" ] || [ "$CI" = "" ]; then
-    local GITURL_VAR="${PROJECT}_CI_GITURL"
-    local GITURL="${!GITURL_VAR}"
-    local REF_VAR="${PROJECT}_CI_REF"
-    local REF="${!REF_VAR}"
     git clone "$GITURL" "$DEST"
     cd "$DEST"
     git checkout "$REF"
   else # When possible, we download tarballs to reduce bandwidth and latency
     local ARCHIVEURL_VAR="${PROJECT}_CI_ARCHIVEURL"
     local ARCHIVEURL="${!ARCHIVEURL_VAR}"
-    local REF_VAR="${PROJECT}_CI_REF"
-    local REF="${!REF_VAR}"
     mkdir -p "$DEST"
     cd "$DEST"
-    wget "$ARCHIVEURL/$REF.tar.gz"
-    tar xvfz "$REF.tar.gz" --strip-components=1
-    rm -f "$REF.tar.gz"
+    local COMMIT=$(git ls-remote "$GITURL" "refs/heads/$REF" | cut -f 1)
+    if [[ "$COMMIT" == "" ]]; then
+      # $REF must have been a tag or hash, not a branch
+      COMMIT="$REF"
+    fi
+    wget "$ARCHIVEURL/$COMMIT.tar.gz"
+    tar xvfz "$COMMIT.tar.gz" --strip-components=1
+    rm -f "$COMMIT.tar.gz"
   fi
 }
 
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat_parsers.sh
index ac74ebf667..ac74ebf667 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat_parsers.sh
diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh
index 12a70176c2..9ca8f76054 100755
--- a/dev/ci/ci-wrapper.sh
+++ b/dev/ci/ci-wrapper.sh
@@ -6,13 +6,6 @@
 
 set -eo pipefail
 
-function travis_fold {
-    if [ -n "${TRAVIS}" ];
-    then
-	echo "travis_fold:$1:$2"
-    fi
-}
-
 CI_NAME="$1"
 CI_SCRIPT="ci-${CI_NAME}.sh"
 
@@ -22,6 +15,5 @@ cd "${DIR}/../.."
 
 export TIMED=1
 "${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log
-travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...'
+echo 'Aggregating timing log...'
 python ./tools/make-one-time-file.py time-of-build.log
-travis_fold 'end' 'coq.test.timing'
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index baf470e021..43278c37b1 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-02-17-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"
@@ -56,9 +56,6 @@ ENV COMPILER_EDGE="4.07.1" \
     COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \
     BASE_OPAM_EDGE="dune-release.1.1.0"
 
-RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \
-    opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE
-
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
 RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \
diff --git a/dev/ci/nix/CoLoR.nix b/dev/ci/nix/CoLoR.nix
index 4c5cfd83da..3fcf177aec 100644
--- a/dev/ci/nix/CoLoR.nix
+++ b/dev/ci/nix/CoLoR.nix
@@ -1,5 +1,5 @@
 { bignums }:
 
 {
-  buildInputs = [ bignums ];
+  coqBuildInputs = [ bignums ];
 }
diff --git a/dev/ci/nix/Corn.nix b/dev/ci/nix/Corn.nix
index 18c7750279..0d22a6b91b 100644
--- a/dev/ci/nix/Corn.nix
+++ b/dev/ci/nix/Corn.nix
@@ -1,5 +1,5 @@
 { bignums, math-classes }:
 
 {
-  buildInputs = [ bignums math-classes ];
+  coqBuildInputs = [ bignums math-classes ];
 }
diff --git a/dev/ci/nix/GeoCoq.nix b/dev/ci/nix/GeoCoq.nix
index a86fb2c44a..45d688285e 100644
--- a/dev/ci/nix/GeoCoq.nix
+++ b/dev/ci/nix/GeoCoq.nix
@@ -1,5 +1,5 @@
 { mathcomp }:
 {
-  buildInputs = [ mathcomp ];
+  coqBuildInputs = [ mathcomp ];
   configure = "./configure.sh";
 }
diff --git a/dev/ci/nix/README.md b/dev/ci/nix/README.md
index 1685b084e9..6f32abef95 100644
--- a/dev/ci/nix/README.md
+++ b/dev/ci/nix/README.md
@@ -17,3 +17,10 @@ build-system of that project: `configure`, `make`, and `clean`. Therefore, after
 changing the working directory to the root of the sources of that project, the
 contents of these variables can be evaluated to respectively set-up, build, and
 clean the project.
+
+## Variant: nocoq
+
+The dependencies of the third-party developments are split into `buildInputs`
+and `coqBuildInputs`. The second list gathers the Coq libraries. In case you
+only want the non-coq dependencies (because you want to use Coq from your `PATH`),
+set the environment variable `NOCOQ` to some non-empty value.
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 4acfae48e4..94e0a666e2 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -2,7 +2,8 @@
 , branch
 , wd
 , project ? "xyz"
-, bn ? "release"
+, withCoq ? true
+, bn ? "master"
 }:
 
 with pkgs;
@@ -16,6 +17,11 @@ let mathcomp = coqPackages.mathcomp.overrideAttrs (o: {
     name = "coq-git-mathcomp-git";
     src = fetchTarball https://github.com/math-comp/math-comp/archive/master.tar.gz;
   }); in
+let ssreflect = coqPackages.ssreflect.overrideAttrs (o: {
+  inherit (mathcomp) src;
+  }); in
+let coq-ext-lib = coqPackages.coq-ext-lib; in
+let simple-io = coqPackages.simple-io; in
 let bignums = coqPackages.bignums.overrideAttrs (o:
     if bn == "release" then {} else
     if bn == "master" then { src = fetchTarball https://github.com/coq/bignums/archive/master.tar.gz; } else
@@ -28,9 +34,27 @@ let math-classes =
     src = fetchTarball "https://github.com/coq-community/math-classes/archive/master.tar.gz";
   }); in
 
-let unicoq = callPackage ./unicoq.nix { inherit coq; }; in
+let corn = (coqPackages.corn.override { inherit coq bignums math-classes; })
+  .overrideAttrs (o: {
+    src = fetchTarball "https://github.com/coq-community/corn/archive/master.tar.gz";
+  }); in
 
-let callPackage = newScope { inherit coq mathcomp bignums coqprime math-classes unicoq; }; in
+let stdpp = coqPackages.stdpp.overrideAttrs (o: {
+    src = fetchTarball "https://gitlab.mpi-sws.org/iris/stdpp/-/archive/master/stdpp-master.tar.bz2";
+  }); in
+
+let iris = (coqPackages.iris.override { inherit coq stdpp; })
+  .overrideAttrs (o: {
+    src = fetchTarball "https://gitlab.mpi-sws.org/iris/iris/-/archive/master/iris-master.tar.bz2";
+    propagatedBuildInputs = [ stdpp ];
+  }); in
+
+let unicoq = callPackage ./unicoq { inherit coq; }; in
+
+let callPackage = newScope { inherit coq
+  bignums coq-ext-lib coqprime corn iris math-classes
+  mathcomp simple-io ssreflect stdpp unicoq;
+}; in
 
 # Environments for building CI libraries with this Coq
 let projects = {
@@ -45,12 +69,16 @@ let projects = {
   fiat_crypto = callPackage ./fiat_crypto.nix {};
   fiat_crypto_legacy = callPackage ./fiat_crypto_legacy.nix {};
   flocq = callPackage ./flocq.nix {};
+  formal-topology = callPackage ./formal-topology.nix {};
   GeoCoq = callPackage ./GeoCoq.nix {};
   HoTT = callPackage ./HoTT.nix {};
+  iris = callPackage ./iris.nix {};
+  lambda-rust = callPackage ./lambda-rust.nix {};
   math_classes = callPackage ./math_classes.nix {};
   mathcomp = {};
   mtac2 = callPackage ./mtac2.nix {};
   oddorder = callPackage ./oddorder.nix {};
+  quickchick = callPackage ./quickchick.nix {};
   VST = callPackage ./VST.nix {};
 }; in
 
@@ -60,10 +88,16 @@ else
 
 let prj = projects."${project}"; in
 
+let inherit (stdenv.lib) optional optionals; in
+
 stdenv.mkDerivation {
   name = "shell-for-${project}-in-${branch}";
 
-  buildInputs = [ coq ] ++ (prj.buildInputs or []);
+  buildInputs =
+    optional withCoq coq
+  ++ (prj.buildInputs or [])
+  ++ optionals withCoq (prj.coqBuildInputs or [])
+  ;
 
   configure = prj.configure or "true";
   make = prj.make or "make";
diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix
index 7b37e6e8e4..0f0ee91387 100644
--- a/dev/ci/nix/fiat_crypto.nix
+++ b/dev/ci/nix/fiat_crypto.nix
@@ -1,6 +1,6 @@
 { coqprime }:
 {
-  buildInputs = [ coqprime ];
+  coqBuildInputs = [ coqprime ];
   configure = "git submodule update --init --recursive && ulimit -s 32768";
   make = "make new-pipeline c-files";
 }
diff --git a/dev/ci/nix/formal-topology.nix b/dev/ci/nix/formal-topology.nix
new file mode 100644
index 0000000000..53b9b1182b
--- /dev/null
+++ b/dev/ci/nix/formal-topology.nix
@@ -0,0 +1,4 @@
+{ corn }:
+{
+  coqBuildInputs = [ corn ];
+}
diff --git a/dev/ci/nix/iris.nix b/dev/ci/nix/iris.nix
new file mode 100644
index 0000000000..b55cccc7c6
--- /dev/null
+++ b/dev/ci/nix/iris.nix
@@ -0,0 +1,4 @@
+{ stdpp }:
+{
+  coqBuildInputs = [ stdpp ];
+}
diff --git a/dev/ci/nix/lambda-rust.nix b/dev/ci/nix/lambda-rust.nix
new file mode 100644
index 0000000000..0d07c3028a
--- /dev/null
+++ b/dev/ci/nix/lambda-rust.nix
@@ -0,0 +1,4 @@
+{ iris }:
+{
+  coqBuildInputs = [ iris ];
+}
diff --git a/dev/ci/nix/math_classes.nix b/dev/ci/nix/math_classes.nix
index b0fa2fe795..8edc3c8358 100644
--- a/dev/ci/nix/math_classes.nix
+++ b/dev/ci/nix/math_classes.nix
@@ -1,6 +1,6 @@
 { bignums }:
 
 {
-  buildInputs = [ bignums ];
+  coqBuildInputs = [ bignums ];
   configure = "./configure.sh";
 }
diff --git a/dev/ci/nix/mtac2.nix b/dev/ci/nix/mtac2.nix
index 9a2353c5cf..4acc326c02 100644
--- a/dev/ci/nix/mtac2.nix
+++ b/dev/ci/nix/mtac2.nix
@@ -1,5 +1,6 @@
 { coq, unicoq }:
 {
-  buildInputs = [ unicoq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]);
+  buildInputs = with coq.ocamlPackages; [ ocaml findlib camlp5 ];
+  coqBuildInputs = [ unicoq ];
   configure = "./configure.sh";
 }
diff --git a/dev/ci/nix/oddorder.nix b/dev/ci/nix/oddorder.nix
index 3b8fdbab51..2341bb3173 100644
--- a/dev/ci/nix/oddorder.nix
+++ b/dev/ci/nix/oddorder.nix
@@ -1,4 +1,4 @@
 { mathcomp }:
 {
-  buildInputs = [ mathcomp ];
+  coqBuildInputs = [ mathcomp ];
 }
diff --git a/dev/ci/nix/quickchick.nix b/dev/ci/nix/quickchick.nix
new file mode 100644
index 0000000000..46bf02ae3c
--- /dev/null
+++ b/dev/ci/nix/quickchick.nix
@@ -0,0 +1,5 @@
+{ ocamlPackages, ssreflect, coq-ext-lib, simple-io }:
+{
+  buildInputs = with ocamlPackages; [ ocaml findlib ocamlbuild num ];
+  coqBuildInputs = [ ssreflect coq-ext-lib simple-io ];
+}
diff --git a/dev/ci/nix/shell b/dev/ci/nix/shell
index 2e4462ed40..a5f8ee8f54 100755
--- a/dev/ci/nix/shell
+++ b/dev/ci/nix/shell
@@ -17,4 +17,10 @@ else
   BN=""
 fi
 
-nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN
+if [ "$NOCOQ" ]; then
+    NOCOQ="--arg withCoq false"
+else
+    NOCOQ=""
+fi
+
+nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN $NOCOQ
diff --git a/dev/ci/nix/unicoq.nix b/dev/ci/nix/unicoq.nix
deleted file mode 100644
index 093c262cde..0000000000
--- a/dev/ci/nix/unicoq.nix
+++ /dev/null
@@ -1,11 +0,0 @@
-{ stdenv, coq }:
-
-stdenv.mkDerivation {
-  name = "coq${coq.coq-version}-unicoq-0.0-git";
-  src = fetchTarball https://github.com/unicoq/unicoq/archive/master.tar.gz;
-
-  buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 num ]);
-
-  configurePhase = "coq_makefile -f Make -o Makefile";
-  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
-}
diff --git a/dev/ci/nix/unicoq/default.nix b/dev/ci/nix/unicoq/default.nix
new file mode 100644
index 0000000000..54c67ac0fd
--- /dev/null
+++ b/dev/ci/nix/unicoq/default.nix
@@ -0,0 +1,26 @@
+{ stdenv, writeText, coq }:
+
+let META = writeText "META" ''
+  archive(native) = "unicoq.cmxa"
+  plugin(native) = "unicoq.cmxs"
+''; in
+
+
+stdenv.mkDerivation {
+  name = "coq${coq.coq-version}-unicoq-0.0-git";
+  src = fetchTarball https://github.com/unicoq/unicoq/archive/master.tar.gz;
+
+  patches = [ ./unicoq-num.patch ];
+
+  buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 num ]);
+
+  configurePhase = "coq_makefile -f Make -o Makefile";
+  installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
+
+  postInstall = ''
+    cp ${META} META
+    install -d $OCAMLFIND_DESTDIR
+    ln -s $out/lib/coq/${coq.coq-version}/user-contrib/Unicoq $OCAMLFIND_DESTDIR/
+    install -m 0644 META src/unicoq.a $OCAMLFIND_DESTDIR/Unicoq
+  '';
+}
diff --git a/dev/ci/nix/unicoq/unicoq-num.patch b/dev/ci/nix/unicoq/unicoq-num.patch
new file mode 100644
index 0000000000..6d96d94dfc
--- /dev/null
+++ b/dev/ci/nix/unicoq/unicoq-num.patch
@@ -0,0 +1,44 @@
+commit f29bc64ee3d8b36758d17e1f5d50812e0c93063b
+Author: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
+Date:   Thu Nov 29 08:59:22 2018 +0000
+
+    Make explicit dependency to num
+
+diff --git a/Make b/Make
+index 550dc6a..8aa1309 100644
+--- a/Make
++++ b/Make
+@@ -9,7 +9,7 @@ src/logger.ml
+ src/munify.mli
+ src/munify.ml
+ src/unitactics.mlg
+-src/unicoq.mllib
++src/unicoq.mlpack
+ theories/Unicoq.v
+ test-suite/munifytest.v
+ test-suite/microtests.v
+diff --git a/Makefile.local b/Makefile.local
+new file mode 100644
+index 0000000..88be365
+--- /dev/null
++++ b/Makefile.local
+@@ -0,0 +1 @@
++CAMLPKGS += -package num
+diff --git a/src/unicoq.mllib b/src/unicoq.mllib
+deleted file mode 100644
+index 2b84e2d..0000000
+--- a/src/unicoq.mllib
++++ /dev/null
+@@ -1,3 +0,0 @@
+-Logger
+-Munify
+-Unitactics
+diff --git a/src/unicoq.mlpack b/src/unicoq.mlpack
+new file mode 100644
+index 0000000..2b84e2d
+--- /dev/null
++++ b/src/unicoq.mlpack
+@@ -0,0 +1,3 @@
++Logger
++Munify
++Unitactics
diff --git a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh
deleted file mode 100644
index 2df8affd14..0000000000
--- a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9102" ] || [ "$CI_BRANCH" = "ltac+remove_aliases" ]; then
-
-    elpi_CI_REF=ltac+remove_aliases
-    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh b/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh
deleted file mode 100644
index f2a113b118..0000000000
--- a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9150" ] || [ "$CI_BRANCH" = "build+warn_50" ]; then
-
-    mtac2_CI_REF=build+warn_50
-    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh
deleted file mode 100644
index f532fdfc52..0000000000
--- a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9172" ] || [ "$CI_BRANCH" = "proof_rework" ]; then
-
-    ltac2_CI_REF=proof_rework
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
-    mtac2_CI_REF=proof_rework
-    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh
new file mode 100644
index 0000000000..23eb24c304
--- /dev/null
+++ b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "9173" ] || [ "$CI_BRANCH" = "proofview+proof_info" ]; then
+
+    ltac2_CI_REF=proofview+proof_info
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+    fiat_parsers_CI_REF=proofview+proof_info
+    fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat
+
+fi
diff --git a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh b/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh
deleted file mode 100644
index efcdd2e97f..0000000000
--- a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9220" ] || [ "$CI_BRANCH" = "stm-shallow-logic" ]; then
-
-    paramcoq_CI_REF=stm-shallow-logic
-    paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq
-
-fi
diff --git a/dev/ci/user-overlays/09439-sep-variance.sh b/dev/ci/user-overlays/09439-sep-variance.sh
new file mode 100644
index 0000000000..cca85a2f68
--- /dev/null
+++ b/dev/ci/user-overlays/09439-sep-variance.sh
@@ -0,0 +1,14 @@
+
+if [ "$CI_PULL_REQUEST" = "9439" ] || [ "$CI_BRANCH" = "sep-variance" ]; then
+    elpi_CI_REF=sep-variance
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+    equations_CI_REF=sep-variance
+    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+    mtac2_CI_REF=sep-variance
+    mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2
+
+    paramcoq_CI_REF=sep-variance
+    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+fi