8 files changed, 24 insertions, 59 deletions
diff --git a/dev/base_include b/dev/base_include
index f9af0696b1..8ee1cceb23 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -58,8 +58,6 @@
 
 (* Open main files *)
 
-open API
-open Grammar_API
 open Names
 open Term
 open Vars
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index f1e1515d41..5435e95885 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -18,7 +18,9 @@ ls "$COQBIN"
 # Where we clone and build external developments
 CI_BUILD_DIR=`pwd`/_build_ci
 
-source ${ci_dir}/ci-user-overlay.sh
+for overlay in ${ci_dir}/user-overlays/*.sh; do
+  source ${overlay}
+done
 source ${ci_dir}/ci-basic-overlay.sh
 
 mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
deleted file mode 100644
index b242ce3bd9..0000000000
--- a/dev/ci/ci-user-overlay.sh
+++ /dev/null
@@ -1,54 +0,0 @@
-#!/usr/bin/env bash
-
-# Add user overlays here. You can use some logic to detect if you are
-# in your travis branch and conditionally enable the overlay.
-
-# Some useful Travis variables:
-# (https://docs.travis-ci.com/user/environment-variables/#Default-Environment-Variables)
-#
-# - TRAVIS_BRANCH: For builds not triggered by a pull request this is
-#   the name of the branch currently being built; whereas for builds
-#   triggered by a pull request this is the name of the branch
-#   targeted by the pull request (in many cases this will be master).
-#
-# - TRAVIS_COMMIT: The commit that the current build is testing.
-#
-# - TRAVIS_PULL_REQUEST: The pull request number if the current job is
-#   a pull request, “false” if it’s not a pull request.
-#
-# - TRAVIS_PULL_REQUEST_BRANCH: If the current job is a pull request,
-#   the name of the branch from which the PR originated. "" if the
-#   current job is a push build.
-
-echo $TRAVIS_PULL_REQUEST_BRANCH
-echo $TRAVIS_PULL_REQUEST
-echo $TRAVIS_BRANCH
-echo $TRAVIS_COMMIT
-
-if [ $TRAVIS_PULL_REQUEST == "669" ] || [ $TRAVIS_BRANCH == "ssr-merge" ]; then
-    mathcomp_CI_BRANCH=ssr-merge
-    mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
-fi
-
-echo "DEBUG: ci-user-overlay.sh 0"
-if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_makefile" ]; then
-    echo "DEBUG: ci-user-overlay.sh 1"
-    fiat_parsers_CI_BRANCH=trunk__API
-    fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git
-fi
-
-if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums" ]; then
-    math_classes_CI_BRANCH=external-bignums
-    math_classes_CI_GITURL=https://github.com/letouzey/math-classes.git
-    Corn_CI_BRANCH=external-bignums
-    Corn_CI_GITURL=https://github.com/letouzey/corn.git
-fi
-
-if [ $TRAVIS_PULL_REQUEST == "220" ] || [ $TRAVIS_BRANCH == "less_init_plugins" ]; then
-    CompCert_CI_BRANCH=less_init_plugins
-    CompCert_CI_GITURL=https://github.com/letouzey/CompCert.git
-    VST_CI_BRANCH=less_init_plugins
-    VST_CI_GITURL=https://github.com/letouzey/VST.git
-    fiat_crypto_CI_BRANCH=less_init_plugins
-    fiat_crypto_CI_GITURL=https://github.com/letouzey/fiat-crypto.git
-fi
diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
new file mode 100644
index 0000000000..af4a96f4ae
--- /dev/null
+++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
@@ -0,0 +1,4 @@
+if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then
+    mathcomp_CI_BRANCH=ssr-merge
+    mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
+fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
new file mode 100644
index 0000000000..9146d3d521
--- /dev/null
+++ b/dev/ci/user-overlays/README.md
@@ -0,0 +1,14 @@
+# Add overlays for your pull requests in this directory
+
+An overlay is a file containing very simple logic to test whether we are currently building a specific pull request or git branch (useful so that overlays work on your own fork) and which changes some of the variables whose default can be found in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh).
+
+The name of your overlay file should be of the form `five_digit_PR_number-GitHub_handle-branch_name.sh`.
+
+Example: `00669-maximedenes-ssr-merge.sh` containing
+
+```
+if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then
+    mathcomp_CI_BRANCH=ssr-merge
+    mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
+fi
+```
diff --git a/dev/include b/dev/include
index 0f43f00729..31ae5da71a 100644
--- a/dev/include
+++ b/dev/include
@@ -41,6 +41,8 @@
 #install_printer  (* univ context *) ppuniverse_context;;
 #install_printer  (* univ context future *) ppuniverse_context_future;;
 #install_printer  (* univ context set *) ppuniverse_context_set;;
+#install_printer  (* cumulativity info *) ppcumulativity_info;;
+#install_printer  (* abstract cumulativity info *) ppabstract_cumulativity_info;;
 #install_printer  (* univ set *) ppuniverse_set;;
 #install_printer  (* univ instance *) ppuniverse_instance;;
 #install_printer  (* univ subst *) ppuniverse_subst;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 6ae5125f6d..ff575e432c 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -8,7 +8,6 @@
 
 (* Printers for the ocaml toplevel. *)
 
-open API
 open Util
 open Pp
 open Names
@@ -215,6 +214,7 @@ let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
 let ppuniverse_context_future c = 
   let ctx = Future.force c in
     ppuniverse_context ctx
+let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c)
 let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
 let ppnamedcontextval e =
   pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e))
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index be6b914b6b..afa94a63e0 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -1,4 +1,3 @@
-open API
 open Format
 open Term
 open Names