8 files changed, 32 insertions, 39 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 7ed90f524c..bc49e3e76b 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -84,10 +84,10 @@ unless these tests pass.
 
 We are currently running tests on the following platforms:
 
-- GitLab CI is the main CI platform. It tests the compilation of Coq, of the
-  documentation, and of CoqIDE on Linux with several versions of OCaml /
-  camlp5, and with warnings as errors; it runs the test-suite and tests the
-  compilation of several external developments.
+- GitLab CI is the main CI platform. It tests the compilation of Coq,
+  of the documentation, and of CoqIDE on Linux with several versions
+  of OCaml and with warnings as errors; it runs the test-suite and
+  tests the compilation of several external developments.
 
 - Travis CI is used to test the compilation of Coq and run the test-suite on
   macOS. It also runs a linter that checks whitespace discipline. A
diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh
index 84fec71f7a..abeb039c0e 100644
--- a/dev/ci/appveyor.sh
+++ b/dev/ci/appveyor.sh
@@ -10,6 +10,6 @@ bash opam64/install.sh
 
 opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $APPVEYOR_OPAM_SWITCH --switch $APPVEYOR_OPAM_SWITCH
 eval "$(opam config env)"
-opam install -y num ocamlfind camlp5 ounit
+opam install -y num ocamlfind ounit
 
 cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= # && make validate
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 4d5834eeb6..96bc5be7ff 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -215,13 +215,6 @@
 : "${fcsl_pcm_CI_ARCHIVEURL:=${fcsl_pcm_CI_GITURL}/archive}"
 
 ########################################################################
-# pidetop
-########################################################################
-: "${pidetop_CI_REF:=v8.9}"
-: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop}"
-: "${pidetop_CI_ARCHIVEURL:=${pidetop_CI_GITURL}/get}"
-
-########################################################################
 # ext-lib
 ########################################################################
 : "${ext_lib_CI_REF:=master}"
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
deleted file mode 100755
index 1a9a26843c..0000000000
--- a/dev/ci/ci-pidetop.sh
+++ /dev/null
@@ -1,19 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-git_download pidetop
-
-# Travis / Gitlab have different filesystem layout due to use of
-# `-local`. We need to improve this divergence but if we use Dune this
-# "local" oddity goes away automatically so not bothering...
-if [ -d "$COQBIN/../lib/coq" ]; then
-   COQLIB="$COQBIN/../lib/coq/"
-else
-   COQLIB="$COQBIN/../"
-fi
-
-( cd "${CI_BUILD_DIR}/pidetop" && dune build -p pidetop @install )
-
-echo -en '4\nexit' | "${CI_BUILD_DIR}/pidetop/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 4ddb582414..3fc6dce4e5 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-10-30-V1"
+# CACHEKEY: "bionic_coq-V2018-11-08-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -41,29 +41,27 @@ ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.4.0 ounit.2.0.8 odoc.1.3.0" \
     CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
-ENV CAMLP5_VER="7.03" \
-    COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
+ENV COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
 
 # base switch
 RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \
-    opam install $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM
+    opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM
 
 # base+32bit switch
 RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
-    opam install $BASE_OPAM camlp5.$CAMLP5_VER
+    opam install $BASE_OPAM
 
 # EDGE switch
 ENV COMPILER_EDGE="4.07.1" \
-    CAMLP5_VER_EDGE="7.06.10-g84ce6cc4" \
     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 camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE
+    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) && \
-    opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM
+    opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE $CI_OPAM
 
 RUN opam clean -a -c
diff --git a/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh b/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh
new file mode 100644
index 0000000000..d7130cc67a
--- /dev/null
+++ b/dev/ci/user-overlays/08985-ejgallego-build+pack_gramlib.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "8985" ] || [ "$CI_BRANCH" = "build+pack_gramlib" ]; then
+
+    elpi_CI_REF=use_coq_gramlib
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh
new file mode 100644
index 0000000000..c8bea0c868
--- /dev/null
+++ b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "8998" ] || [ "$CI_BRANCH" = "legacy_proof_eng_clean" ]; then
+
+    equations_CI_REF=legacy_proof_eng_clean
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh b/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh
new file mode 100644
index 0000000000..14e7c0d7f0
--- /dev/null
+++ b/dev/ci/user-overlays/09051-ppedrot-camlp5-safe-api-strikes-back.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "9051" ] || [ "$CI_BRANCH" = "camlp5-safe-api-strikes-back" ]; then
+
+    equations_CI_REF=camlp5-safe-api-strikes-back
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+    ltac2_CI_REF=camlp5-safe-api-strikes-back
+    ltac2_CI_GITURL=https://github.com/ppedrot/ltac2
+
+fi