13 files changed, 211 insertions, 53 deletions
diff --git a/dev/checker.dbg b/dev/checker.dbg
new file mode 100644
index 0000000000..b2323b6175
--- /dev/null
+++ b/dev/checker.dbg
@@ -0,0 +1,6 @@
+load_printer threads.cma
+load_printer str.cma
+load_printer clib.cma
+load_printer dynlink.cma
+load_printer lib.cma
+load_printer check.cma
diff --git a/dev/checker_db b/dev/checker_db
new file mode 100644
index 0000000000..327e636c57
--- /dev/null
+++ b/dev/checker_db
@@ -0,0 +1,39 @@
+source checker.dbg
+
+load_printer checker_printers.cmo
+
+install_printer Checker_printers.pP
+
+install_printer Checker_printers.ppfuture
+
+install_printer Checker_printers.ppid
+install_printer Checker_printers.pplab
+install_printer Checker_printers.ppmbid
+install_printer Checker_printers.ppdir
+install_printer Checker_printers.ppmp
+install_printer Checker_printers.ppcon
+install_printer Checker_printers.ppproj
+install_printer Checker_printers.ppkn
+install_printer Checker_printers.ppmind
+install_printer Checker_printers.ppind
+
+install_printer Checker_printers.ppbigint
+
+install_printer Checker_printers.ppintset
+install_printer Checker_printers.ppidset
+
+install_printer Checker_printers.ppidmapgen
+
+install_printer Checker_printers.ppididmap
+
+install_printer Checker_printers.ppuni
+install_printer Checker_printers.ppuni_level
+install_printer Checker_printers.ppuniverse_set
+install_printer Checker_printers.ppuniverse_instance
+install_printer Checker_printers.ppauniverse_context
+install_printer Checker_printers.ppuniverse_context
+install_printer Checker_printers.ppconstraints
+install_printer Checker_printers.ppuniverse_context_future
+install_printer Checker_printers.ppuniverses
+
+install_printer Checker_printers.pploc
diff --git a/dev/checker_printers.ml b/dev/checker_printers.ml
new file mode 100644
index 0000000000..40ae1a7b05
--- /dev/null
+++ b/dev/checker_printers.ml
@@ -0,0 +1,73 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Pp
+open Names
+open Univ
+
+let pp   x = Pp.pp_with Format.std_formatter x
+
+(** Future printer *)
+
+let ppfuture kx = pp (Future.print (fun _ -> str "_") kx)
+
+(* name printers *)
+let ppid id = pp (Id.print id)
+let pplab l = pp (Label.print l)
+let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
+let ppdir dir = pp (DirPath.print dir)
+let ppmp mp = pp(str (ModPath.debug_to_string mp))
+let ppcon con = pp(Constant.debug_print con)
+let ppproj con = pp(Constant.debug_print (Projection.constant con))
+let ppkn kn = pp(str (KerName.to_string kn))
+let ppmind kn = pp(MutInd.debug_print kn)
+let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i)
+
+(* term printers *)
+let ppbigint n = pp (str (Bigint.to_string n));;
+
+let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
+let ppintset l = pp (prset int (Int.Set.elements l))
+let ppidset l = pp (prset Id.print (Id.Set.elements l))
+
+let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]"
+
+let pridmap pr l =
+  let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in
+  prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l [])
+let ppidmap pr l = pp (pridmap pr l)
+
+let pridmapgen l =
+  let dom = Id.Set.elements (Id.Map.domain l) in
+  if dom = [] then str "[]" else
+  str "[domain= " ++ hov 0 (prlist_with_sep spc Id.print dom) ++ str "]"
+let ppidmapgen l = pp (pridmapgen l)
+
+let prididmap = pridmap (fun _ -> Id.print)
+let ppididmap = ppidmap (fun _ -> Id.print)
+
+let pP s = pp (hov 0 s)
+
+(* proof printers *)
+let ppuni u = pp(Universe.pr u)
+let ppuni_level u = pp (Level.pr u)
+
+let ppuniverse_set l = pp (LSet.pr l)
+let ppuniverse_instance l = pp (Instance.pr l)
+let ppauniverse_context l = pp (AUContext.pr Level.pr l)
+let ppuniverse_context l = pp (pr_universe_context Level.pr l)
+let ppconstraints c = pp (pr_constraints Level.pr c)
+let ppuniverse_context_future c =
+  let ctx = Future.force c in
+    ppuniverse_context ctx
+let ppuniverses u = pp (Univ.pr_universes u)
+
+let pploc x = let (l,r) = Loc.unloc x in
+  print_string"(";print_int l;print_string",";print_int r;print_string")"
diff --git a/dev/checker_printers.mli b/dev/checker_printers.mli
new file mode 100644
index 0000000000..2f9500c5c3
--- /dev/null
+++ b/dev/checker_printers.mli
@@ -0,0 +1,54 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Printers for the ocaml toplevel. *)
+
+val pp : Pp.t -> unit
+val pP : Pp.t -> unit (* with surrounding box *)
+
+val ppfuture : 'a Future.computation -> unit
+
+val ppid : Names.Id.t -> unit
+val pplab : Names.Label.t -> unit
+val ppmbid : Names.MBId.t -> unit
+val ppdir : Names.DirPath.t -> unit
+val ppmp : Names.ModPath.t -> unit
+val ppcon : Names.Constant.t -> unit
+val ppproj : Names.Projection.t -> unit
+val ppkn : Names.KerName.t -> unit
+val ppmind : Names.MutInd.t -> unit
+val ppind : Names.inductive -> unit
+
+val ppbigint : Bigint.bigint -> unit
+
+val ppintset : Int.Set.t -> unit
+val ppidset : Names.Id.Set.t -> unit
+
+val pridmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> Pp.t
+val ppidmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> unit
+
+val pridmapgen : 'a Names.Id.Map.t -> Pp.t
+val ppidmapgen : 'a Names.Id.Map.t -> unit
+
+val prididmap : Names.Id.t Names.Id.Map.t -> Pp.t
+val ppididmap : Names.Id.t Names.Id.Map.t -> unit
+
+(* Universes *)
+val ppuni : Univ.Universe.t -> unit
+val ppuni_level : Univ.Level.t -> unit (* raw *)
+val ppuniverse_set : Univ.LSet.t -> unit
+val ppuniverse_instance : Univ.Instance.t -> unit
+val ppauniverse_context : Univ.AUContext.t -> unit
+val ppuniverse_context : Univ.UContext.t -> unit
+val ppconstraints : Univ.Constraint.t -> unit
+val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
+val ppuniverses : Univ.universes -> unit
+
+val pploc : Loc.t -> unit
diff --git a/dev/ci/README.md b/dev/ci/README.md
index dee3d2aff7..ed3442e0db 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -141,7 +141,6 @@ no OCaml warnings build Coq in parallel with other tests.
 
 ### GitLab and Windows
 
-
 If your repository has access to runners tagged `windows`, setting the
 secret variable `WINDOWS` to `enabled` will add jobs building Windows
 versions of Coq (32bit and 64bit).
@@ -155,6 +154,10 @@ System and opam packages are installed in a Docker image. The image is
 automatically built and uploaded to your GitLab registry, and is
 loaded by subsequent jobs.
 
+**IMPORTANT**: When updating Coq's CI docker image, you must modify
+the `CACHEKEY` variable in `.gitlab-ci.yml`, `.circleci/config.yml`,
+and `Dockerfile`.
+
 The Docker building job reuses the uploaded image if it is available,
 but if you wish to save more time you can skip the job by setting
 `SKIP_DOCKER` to `true`.
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 5d96c24991..feabf72d48 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -9,5 +9,6 @@ git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypt
 
 ( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive )
 
-fiat_crypto_CI_TARGETS="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display"
-( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS} )
+fiat_crypto_CI_TARGETS1="printlite lite lite-display"
+fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display"
+( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS1} && make ${fiat_crypto_CI_TARGETS2} )
diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md
index 8e677f6f2b..919e2a735f 100644
--- a/dev/ci/docker/README.md
+++ b/dev/ci/docker/README.md
@@ -1,37 +1,13 @@
 ## Overall Docker Setup for Coq's CI.
 
 This directory provides Docker images to be used by Coq's CI. The
-images do support Docker autobuild on `hub.docker.com`
+images do support Docker autobuild on `hub.docker.com` and Gitlab's
+private registry.
 
-Autobuild is the preferred build method [see below]; if you are a
-member of the `coqci` organization, the automated build will push the
-image to the `coqci/name:$VERSION` tag using a Docker hub hook.
-
-## Updating the Image and Syncronization with CI files
-
-Unfortunately, at this point some manual synchronization is needed
-between the `Dockerfile` and `.gitlab-ci.yml`. In particular, the
-checklist is:
-
-- check the name and version of the image setup in `hooks/post_push`
-  have to match.
-- check `COMPILER` variables do match.
-
-Once you are sure the variables are right, then proceed to trigger an
-autobuild or do a manual build, et voilà !
-
-## Docker Autobuilding.
-
-We provide basic support for auto-building, see:
-
-https://docs.docker.com/docker-cloud/builds/advanced/
-
-If you are member of the `coqci` Docker organization, trigger an
-autobuild in your account and the image will be pushed to it as we
-set the proper tag in `hooks/post_push`.
-
-We still need to figure out how properly setup a more automated,
-organization-wide auto-building process.
+Gitlab CI will build and tag a Docker by default for every job if the
+`SKIP_DOCKER` variable is not set to `false`. In Coq's CI, this
+variable is usually set to `false` indeed to avoid booting a useless
+job.
 
 ## Manual Building
 
@@ -47,10 +23,6 @@ To upload/push to your hub:
   + `docker tag base:$VERSION $USER/base:$VERSION`
   + `docker push $USER/base:$VERSION`
 
-Now your docker image is ready to be used. To upload to `coqci`:
-- `docker tag base:$VERSION coqci/base:$VERSION`
-- `docker push coqci/base:$VERSION`
-
 ## Debugging / Misc
 
 To open a shell inside an image do `docker run -ti --entrypoint /bin/bash <imageID>`
@@ -62,4 +34,3 @@ end.
 ## Possible Improvements:
 
 - Use ARG for customizing versions, centralize variable setup;
-- Learn more about Docker registry for GITLAB https://gitlab.com/coq/coq/container_registry .
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 689d203a16..a1178ee2a0 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,3 +1,6 @@
+# CACHEKEY: "bionic_coq-V2018-05-07-V2"
+# ^^ Update when modifying this file.
+
 FROM ubuntu:bionic
 LABEL maintainer="e@x80.org"
 
diff --git a/dev/ci/docker/bionic_coq/hooks/post_push b/dev/ci/docker/bionic_coq/hooks/post_push
deleted file mode 100755
index 307680aa51..0000000000
--- a/dev/ci/docker/bionic_coq/hooks/post_push
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/usr/bin/env bash
-
-COQCI_VERSION=V2018-05-07-V2
-docker tag $IMAGE_NAME $DOCKER_REPO:$COQCI_VERSION
-docker push $DOCKER_REPO:$COQCI_VERSION
-
-docker tag $IMAGE_NAME coqci/base:$COQCI_VERSION
-docker push coqci/base:$COQCI_VERSION
diff --git a/dev/core.dbg b/dev/core.dbg
index edf67020ab..972ba701e4 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -2,8 +2,8 @@ source camlp5.dbg
 load_printer threads.cma
 load_printer str.cma
 load_printer clib.cma
-load_printer lib.cma
 load_printer dynlink.cma
+load_printer lib.cma
 load_printer kernel.cma
 load_printer library.cma
 load_printer engine.cma
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 8f1c165dd4..2bec09de2b 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -14,7 +14,15 @@
 
 export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH
 
-exec $OCAMLDEBUG \
+GUESS_CHECKER=
+for arg in "$@"; do
+    if [ "${arg##*/}" = coqchk.byte ]; then
+        GUESS_CHECKER=1
+    fi
+done
+
+if [ -z "$GUESS_CHECKER" ]; then
+    exec $OCAMLDEBUG \
 	-I $CAMLP5LIB -I +threads \
 	-I $COQTOP \
 	-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
@@ -35,3 +43,11 @@ exec $OCAMLDEBUG \
         -I $COQTOP/plugins/xml        -I $COQTOP/plugins/ltac \
         -I $COQTOP/ide \
 	"$@"
+else
+    exec $OCAMLDEBUG \
+        -I $CAMLP5LIB -I +threads \
+        -I $COQTOP \
+        -I $COQTOP/config -I $COQTOP/clib \
+        -I $COQTOP/lib -I $COQTOP/checker \
+        "$@"
+fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 8d5b5bef4a..cb1abc4a94 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -203,17 +203,17 @@ let pproof p = pp(Proof.pr_proof p)
 let ppuni u = pp(Universe.pr u)
 let ppuni_level u = pp (Level.pr u)
 
-let prlev = Universes.pr_with_global_universes
+let prlev = UnivNames.pr_with_global_universes
 let ppuniverse_set l = pp (LSet.pr prlev l)
 let ppuniverse_instance l = pp (Instance.pr prlev l)
 let ppuniverse_context l = pp (pr_universe_context prlev l)
 let ppuniverse_context_set l = pp (pr_universe_context_set prlev l)
 let ppuniverse_subst l = pp (Univ.pr_universe_subst l)
-let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l)
+let ppuniverse_opt_subst l = pp (UnivSubst.pr_universe_opt_subst l)
 let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l)
 let ppevar_universe_context l = pp (Termops.pr_evar_universe_context l)
 let ppconstraints c = pp (pr_constraints Level.pr c)
-let ppuniverseconstraints c = pp (Universes.Constraints.pr c)
+let ppuniverseconstraints c = pp (UnivProblem.Set.pr c)
 let ppuniverse_context_future c = 
   let ctx = Future.force c in
     ppuniverse_context ctx
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index c23ba964c2..63d7d58053 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -139,11 +139,11 @@ val ppuniverse_instance : Univ.Instance.t -> unit
 val ppuniverse_context : Univ.UContext.t -> unit
 val ppuniverse_context_set : Univ.ContextSet.t -> unit
 val ppuniverse_subst : Univ.universe_subst -> unit
-val ppuniverse_opt_subst : Universes.universe_opt_subst -> unit
+val ppuniverse_opt_subst : UnivSubst.universe_opt_subst -> unit
 val ppuniverse_level_subst : Univ.universe_level_subst -> unit
 val ppevar_universe_context : UState.t -> unit
 val ppconstraints : Univ.Constraint.t -> unit
-val ppuniverseconstraints : Universes.Constraints.t -> unit
+val ppuniverseconstraints : UnivProblem.Set.t -> unit
 val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
 val ppcumulativity_info : Univ.CumulativityInfo.t -> unit
 val ppabstract_cumulativity_info : Univ.ACumulativityInfo.t -> unit