24 files changed, 274 insertions, 168 deletions
diff --git a/dev/base_db b/dev/base_db
index e18ac534ac..155e9591e0 100644
--- a/dev/base_db
+++ b/dev/base_db
@@ -1,4 +1,5 @@
 source core.dbg
+load_printer ltac_plugin.cmo
 load_printer top_printers.cmo
 install_printer Top_printers.ppid
 install_printer Top_printers.ppsp
diff --git a/dev/checker.dbg b/dev/checker.dbg
index b2323b6175..b5b7f0e6d3 100644
--- a/dev/checker.dbg
+++ b/dev/checker.dbg
@@ -2,5 +2,6 @@ load_printer threads.cma
 load_printer str.cma
 load_printer clib.cma
 load_printer dynlink.cma
+load_printer config.cma
 load_printer lib.cma
 load_printer check.cma
diff --git a/dev/checker_db b/dev/checker_db
index 327e636c57..fcb6f679ed 100644
--- a/dev/checker_db
+++ b/dev/checker_db
@@ -2,38 +2,4 @@ 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
+source checker_printers.dbg
diff --git a/dev/checker_dune_db b/dev/checker_dune_db
new file mode 100644
index 0000000000..cdb6a4b809
--- /dev/null
+++ b/dev/checker_dune_db
@@ -0,0 +1,5 @@
+source checker_dune.dbg
+
+load_printer checker_printers.cma
+
+source checker_printers.dbg
diff --git a/dev/checker_printers.dbg b/dev/checker_printers.dbg
new file mode 100644
index 0000000000..9ebbd74834
--- /dev/null
+++ b/dev/checker_printers.dbg
@@ -0,0 +1,35 @@
+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/ci/README.md b/dev/ci/README.md
index 7853866f62..4709247549 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -26,7 +26,8 @@ our CI. This means that:
 
 On the condition that:
 
-- At the time of the submission, your development works with Coq master branch.
+- At the time of the submission, your development works with Coq's
+  `master` branch.
 
 - Your development is publicly available in a git repository and we can easily
   send patches to you (e.g. through pull / merge requests).
@@ -60,6 +61,19 @@ performance benchmark. Currently this is done by providing an OPAM package
 in https://github.com/coq/opam-coq-archive and opening an issue at
 https://github.com/coq/coq-bench/issues.
 
+### Recommended branching policy.
+
+It is sometimes the case that you will need to maintain a branch of
+your development for particular Coq versions. This is in fact very
+likely if your development includes a Coq ML plugin.
+
+We thus recommend a branching convention that mirrors Coq's branching
+policy. Then, you would have a `master` branch that follows Coq's
+`master`, a `v8.8` branch that works with Coq's `v8.8` branch and so
+on.
+
+This convention will be supported by tools in the future to make some
+developer commands work more seamlessly.
 
 Information for developers
 --------------------------
diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh
index d2176e326c..84fec71f7a 100644
--- a/dev/ci/appveyor.sh
+++ b/dev/ci/appveyor.sh
@@ -12,4 +12,4 @@ opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $A
 eval "$(opam config env)"
 opam install -y num ocamlfind camlp5 ounit
 
-cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate
+cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= # && make validate
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index f257c62dd3..098c950b32 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-10-04-V2"
+# CACHEKEY: "bionic_coq-V2018-10-23-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -37,7 +37,7 @@ ENV COMPILER="4.05.0"
 # Common OPAM packages.
 # `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.2.1 ounit.2.0.8 odoc.1.2.0" \
+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.
@@ -56,7 +56,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 ENV COMPILER_EDGE="4.07.0" \
     CAMLP5_VER_EDGE="7.06" \
     COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \
-    BASE_OPAM_EDGE="dune-release.0.3.0"
+    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
diff --git a/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh b/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh
new file mode 100644
index 0000000000..bd3e1bf7ff
--- /dev/null
+++ b/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh
@@ -0,0 +1,7 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8741" ] || [ "$CI_BRANCH" = "typeclasses-functional-evar_map" ]; then
+    plugin_tutorial_CI_REF=pr8671-fix
+    plugin_tutorial_CI_GITURL=https://github.com/mattam82/plugin_tutorials
+
+fi
diff --git a/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh b/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh
new file mode 100644
index 0000000000..98530c825a
--- /dev/null
+++ b/dev/ci/user-overlays/08684-maximedenes-cleanup-kernel-entries.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "8684" ] || [ "$CI_BRANCH" = "kernel-entries-cleanup" ]; then
+
+    Elpi_CI_REF=kernel-entries-cleanup
+    Elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi
+
+    Equations_CI_REF=kernel-entries-cleanup
+    Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh b/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh
new file mode 100644
index 0000000000..81ed91f52b
--- /dev/null
+++ b/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "8688" ] || [ "$CI_BRANCH" = "master+generalizing-evar-map-printer-over-env" ]; then
+
+    Elpi_CI_REF=master+generalized-evar-printers-pr8688
+    Elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index 68afe7ee4a..7fb73e447d 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -33,3 +33,11 @@ fi
 ```
 
 (`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](../ci-common.sh))
+
+### Branching conventions
+
+We suggest you use the convention of identical branch names for the
+Coq branch and the CI project branch used in the overlay. For example,
+if your Coq PR is coming from the branch `more_efficient_tc`, and that
+breaks `ltac2`, we suggest you create a `ltac2` overlay with a branch
+named `more_efficient_tc`.
diff --git a/dev/core.dbg b/dev/core.dbg
index 972ba701e4..f676b643e4 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -1,6 +1,7 @@
-source camlp5.dbg
 load_printer threads.cma
 load_printer str.cma
+load_printer gramlib.cma
+load_printer config.cma
 load_printer clib.cma
 load_printer dynlink.cma
 load_printer lib.cma
@@ -16,4 +17,3 @@ load_printer tactics.cma
 load_printer vernac.cma
 load_printer stm.cma
 load_printer toplevel.cma
-load_printer ltac_plugin.cmo
diff --git a/dev/core_dune.dbg b/dev/core_dune.dbg
new file mode 100644
index 0000000000..cf9c5bd39a
--- /dev/null
+++ b/dev/core_dune.dbg
@@ -0,0 +1,20 @@
+load_printer threads.cma
+load_printer str.cma
+load_printer gramlib.cma
+load_printer config.cma
+load_printer clib.cma
+load_printer dynlink.cma
+load_printer lib.cma
+load_printer byterun.cma
+load_printer kernel.cma
+load_printer library.cma
+load_printer engine.cma
+load_printer pretyping.cma
+load_printer interp.cma
+load_printer proofs.cma
+load_printer parsing.cma
+load_printer printing.cma
+load_printer tactics.cma
+load_printer vernac.cma
+load_printer stm.cma
+load_printer toplevel.cma
diff --git a/dev/db b/dev/db
index 2f8c13485a..8733c684af 100644
--- a/dev/db
+++ b/dev/db
@@ -1,88 +1,6 @@
 source core.dbg
+
+load_printer ltac_plugin.cmo
 load_printer top_printers.cmo
 
-install_printer Top_printers.pP
-install_printer Top_printers.ppfuture
-install_printer Top_printers.ppid
-install_printer Top_printers.pplab
-install_printer Top_printers.ppmbid
-install_printer Top_printers.ppdir
-install_printer Top_printers.ppmp
-install_printer Top_printers.ppcon
-install_printer Top_printers.ppproj
-install_printer Top_printers.ppkn
-install_printer Top_printers.ppmind
-install_printer Top_printers.ppind
-install_printer Top_printers.ppsp
-install_printer Top_printers.ppqualid
-install_printer Top_printers.ppclindex
-install_printer Top_printers.ppscheme
-install_printer Top_printers.ppwf_paths
-install_printer Top_printers.ppevar
-install_printer Top_printers.ppconstr
-install_printer Top_printers.ppsconstr
-install_printer Top_printers.ppeconstr
-install_printer Top_printers.ppconstr_expr
-install_printer Top_printers.ppglob_constr
-install_printer Top_printers.pppattern
-install_printer Top_printers.ppfconstr
-install_printer Top_printers.ppbigint
-install_printer Top_printers.ppintset
-install_printer Top_printers.ppidset
-install_printer Top_printers.ppidmapgen
-install_printer Top_printers.ppididmap
-install_printer Top_printers.ppconstrunderbindersidmap
-install_printer Top_printers.ppevarsubst
-install_printer Top_printers.ppunbound_ltac_var_map
-install_printer Top_printers.ppclosure
-install_printer Top_printers.ppclosedglobconstr
-install_printer Top_printers.ppclosedglobconstridmap
-install_printer Top_printers.ppglobal
-install_printer Top_printers.ppconst
-install_printer Top_printers.ppvar
-install_printer Top_printers.ppj
-install_printer Top_printers.ppsubst
-install_printer Top_printers.ppdelta
-install_printer Top_printers.pp_idpred
-install_printer Top_printers.pp_cpred
-install_printer Top_printers.pp_transparent_state
-install_printer Top_printers.pp_stack_t
-install_printer Top_printers.pp_cst_stack_t
-install_printer Top_printers.pp_state_t
-install_printer Top_printers.ppmetas
-install_printer Top_printers.ppevm
-install_printer Top_printers.ppexistentialset
-install_printer Top_printers.ppexistentialfilter
-install_printer Top_printers.ppclenv
-install_printer Top_printers.ppgoalgoal
-install_printer Top_printers.ppgoal
-install_printer Top_printers.pphintdb
-install_printer Top_printers.ppproofview
-install_printer Top_printers.ppopenconstr
-install_printer Top_printers.pproof
-install_printer Top_printers.ppuni
-install_printer Top_printers.ppuni_level
-install_printer Top_printers.ppuniverse_set
-install_printer Top_printers.ppuniverse_instance
-install_printer Top_printers.ppuniverse_context
-install_printer Top_printers.ppuniverse_context_set
-install_printer Top_printers.ppuniverse_subst
-install_printer Top_printers.ppuniverse_opt_subst
-install_printer Top_printers.ppuniverse_level_subst
-install_printer Top_printers.ppevar_universe_context
-install_printer Top_printers.ppconstraints
-install_printer Top_printers.ppuniverseconstraints
-install_printer Top_printers.ppuniverse_context_future
-install_printer Top_printers.ppcumulativity_info
-install_printer Top_printers.ppabstract_cumulativity_info
-install_printer Top_printers.ppuniverses
-install_printer Top_printers.ppnamedcontextval
-install_printer Top_printers.ppenv
-install_printer Top_printers.pptac
-install_printer Top_printers.ppobj
-install_printer Top_printers.pploc
-install_printer Top_printers.pp_argument_type
-install_printer Top_printers.pp_generic_argument
-install_printer Top_printers.ppgenarginfo
-install_printer Top_printers.ppgenargargt
-install_printer Top_printers.ppist
+source top_printers.dbg
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 91ab57f1e9..0aeb30c4e8 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -68,6 +68,27 @@ Note that you must invoke the `#rectypes;;` toplevel flag in order to
 use Coq libraries. The provided `.ocamlinit` file does this
 automatically.
 
+## ocamldebug
+
+You can use `ocamldebug` with Dune; after a build, do:
+
+```
+dune exec dev/dune-dbg
+(ocd) source dune_db
+```
+
+or
+
+```
+dune exec dev/dune-dbg checker
+(ocd) source checker_dune_db
+```
+
+for the checker. Unfortunately, dependency handling here is not fully
+refined, so you need to build enough of Coq once to use this target
+[it will then correctly compute the deps and rebuild if you call the
+script again] This will be fixed in the future.
+
 ## Compositionality, developer and release modes.
 
 By default [in "developer mode"], Dune will compose all the packages
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index fd3101613a..8cefe699cc 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -140,11 +140,9 @@ New files
 For a new file, in most cases, you just have to add it to the proper
 file list(s):
  - For .ml, in the corresponding .mllib (e.g. kernel/kernel.mllib)
-   These files are also used by the experimental ocamlbuild plugin,
-   which is quite touchy about them : be careful with order,
-   duplicated entries, whitespace errors, and do not mention .mli there.
-   If module B depends on module A, then B should be after A in the .mllib
-   file.
+   Be careful with order, duplicated entries, whitespace errors, and
+   do not mention .mli there.  If module B depends on module A, then B
+   should be after A in the .mllib file.
 - For .v, in the corresponding vo.itarget (e.g theories/Init/vo.itarget)
  - The definitions in Makefile.common might have to be adapted too.
  - If your file needs a specific rule, add it to Makefile.build
diff --git a/dev/doc/ocamlbuild.txt b/dev/doc/ocamlbuild.txt
deleted file mode 100644
index efedbc506e..0000000000
--- a/dev/doc/ocamlbuild.txt
+++ /dev/null
@@ -1,30 +0,0 @@
-Ocamlbuild & Coq
-----------------
-
-A quick note in case someone else gets interested someday in compiling
-Coq via ocamlbuild : such an experimental build system has existed
-in the past (more or less maintained from 2009 to 2013), in addition
-to the official build system via gnu make. But this build via
-ocamlbuild has been severly broken since early 2014 (and don't work
-in 8.5, for instance). This experiment has attracted very limited
-interest from other developers over the years, and has been quite
-cumbersome to maintain, so it is now officially discontinued.
-If you want to have a look at the files of this build system
-(especially myocamlbuild.ml), you can fetch :
- - my last effort at repairing this build system (up to coqtop.native) :
-   https://github.com/letouzey/coq-wip/tree/ocamlbuild-partial-repair
- - coq official v8.5 branch (recent but broken)
- - coq v8.4 branch(less up-to-date, but works).
-
-For the record, the three main drawbacks of this experiments were:
- - recurrent issues with circularities reported by ocamlbuild
-   (even though make was happy) during the evolution of Coq sources
- - no proper support of parallel build
- - quite slow re-traversal of already built things
-See the two corresponding bug reports on Mantis, or
-https://github.com/ocaml/ocamlbuild/issues/52
-
-As an interesting feature, I successfully used this to cross-compile
-Coq 8.4 from linux to win32 via mingw.
-
-Pierre Letouzey, june 2016
diff --git a/dev/dune b/dev/dune
new file mode 100644
index 0000000000..fd6c8cf32c
--- /dev/null
+++ b/dev/dune
@@ -0,0 +1,25 @@
+(library
+ (name top_printers)
+ (public_name coq.top_printers)
+ (synopsis "Coq's Debug Printers")
+ (wrapped false)
+ (modules :standard \ checker_printers)
+ (libraries coq.toplevel coq.plugins.ltac))
+
+(library
+ (name checker_printers)
+ (public_name coq.checker_printers)
+ (synopsis "Coq's Debug Printers [for the Checker]")
+ (wrapped false)
+ (flags :standard -open Checklib)
+ (modules checker_printers)
+ (libraries coq.checklib))
+
+(rule
+  (targets dune-dbg)
+  (deps dune-dbg.in
+        ../checker/main.bc
+        ../topbin/coqtop_byte_bin.bc
+        ; This is not enough as the call to `ocamlfind` will fail :/
+        top_printers.cma)
+  (action (copy dune-dbg.in dune-dbg)))
diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in
new file mode 100755
index 0000000000..464e026400
--- /dev/null
+++ b/dev/dune-dbg.in
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+# Run in a proper install dune env.
+case $1 in
+checker)
+  ocamldebug `ocamlfind query -recursive -i-format coq.checker_printers` -I +threads -I dev _build/default/checker/main.bc
+  ;;
+*)
+  ocamldebug `ocamlfind query -recursive -i-format coq.top_printers` -I +threads -I dev _build/default/topbin/coqtop_byte_bin.bc
+  ;;
+esac
diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
index 93b807d5e3..f45f6de529 100644
--- a/dev/dune-workspace.all
+++ b/dev/dune-workspace.all
@@ -1,4 +1,4 @@
-(lang dune 1.2)
+(lang dune 1.4)
 
 ; Add custom flags here. Default developer profile is `dev`
 (context (opam (switch 4.05.0)))
diff --git a/dev/dune_db b/dev/dune_db
new file mode 100644
index 0000000000..f920f7c75c
--- /dev/null
+++ b/dev/dune_db
@@ -0,0 +1,6 @@
+source core_dune.dbg
+
+load_printer ltac_plugin.cma
+load_printer top_printers.cma
+
+source top_printers.dbg
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
new file mode 100644
index 0000000000..eab88c7290
--- /dev/null
+++ b/dev/top_printers.dbg
@@ -0,0 +1,85 @@
+install_printer Top_printers.pP
+install_printer Top_printers.ppfuture
+install_printer Top_printers.ppid
+install_printer Top_printers.pplab
+install_printer Top_printers.ppmbid
+install_printer Top_printers.ppdir
+install_printer Top_printers.ppmp
+install_printer Top_printers.ppcon
+install_printer Top_printers.ppproj
+install_printer Top_printers.ppkn
+install_printer Top_printers.ppmind
+install_printer Top_printers.ppind
+install_printer Top_printers.ppsp
+install_printer Top_printers.ppqualid
+install_printer Top_printers.ppclindex
+install_printer Top_printers.ppscheme
+install_printer Top_printers.ppwf_paths
+install_printer Top_printers.ppevar
+install_printer Top_printers.ppconstr
+install_printer Top_printers.ppsconstr
+install_printer Top_printers.ppeconstr
+install_printer Top_printers.ppconstr_expr
+install_printer Top_printers.ppglob_constr
+install_printer Top_printers.pppattern
+install_printer Top_printers.ppfconstr
+install_printer Top_printers.ppbigint
+install_printer Top_printers.ppintset
+install_printer Top_printers.ppidset
+install_printer Top_printers.ppidmapgen
+install_printer Top_printers.ppididmap
+install_printer Top_printers.ppconstrunderbindersidmap
+install_printer Top_printers.ppevarsubst
+install_printer Top_printers.ppunbound_ltac_var_map
+install_printer Top_printers.ppclosure
+install_printer Top_printers.ppclosedglobconstr
+install_printer Top_printers.ppclosedglobconstridmap
+install_printer Top_printers.ppglobal
+install_printer Top_printers.ppconst
+install_printer Top_printers.ppvar
+install_printer Top_printers.ppj
+install_printer Top_printers.ppsubst
+install_printer Top_printers.ppdelta
+install_printer Top_printers.pp_idpred
+install_printer Top_printers.pp_cpred
+install_printer Top_printers.pp_transparent_state
+install_printer Top_printers.pp_stack_t
+install_printer Top_printers.pp_cst_stack_t
+install_printer Top_printers.pp_state_t
+install_printer Top_printers.ppmetas
+install_printer Top_printers.ppevm
+install_printer Top_printers.ppexistentialset
+install_printer Top_printers.ppexistentialfilter
+install_printer Top_printers.ppclenv
+install_printer Top_printers.ppgoalgoal
+install_printer Top_printers.ppgoal
+install_printer Top_printers.pphintdb
+install_printer Top_printers.ppproofview
+install_printer Top_printers.ppopenconstr
+install_printer Top_printers.pproof
+install_printer Top_printers.ppuni
+install_printer Top_printers.ppuni_level
+install_printer Top_printers.ppuniverse_set
+install_printer Top_printers.ppuniverse_instance
+install_printer Top_printers.ppuniverse_context
+install_printer Top_printers.ppuniverse_context_set
+install_printer Top_printers.ppuniverse_subst
+install_printer Top_printers.ppuniverse_opt_subst
+install_printer Top_printers.ppuniverse_level_subst
+install_printer Top_printers.ppevar_universe_context
+install_printer Top_printers.ppconstraints
+install_printer Top_printers.ppuniverseconstraints
+install_printer Top_printers.ppuniverse_context_future
+install_printer Top_printers.ppcumulativity_info
+install_printer Top_printers.ppabstract_cumulativity_info
+install_printer Top_printers.ppuniverses
+install_printer Top_printers.ppnamedcontextval
+install_printer Top_printers.ppenv
+install_printer Top_printers.pptac
+install_printer Top_printers.ppobj
+install_printer Top_printers.pploc
+install_printer Top_printers.pp_argument_type
+install_printer Top_printers.pp_generic_argument
+install_printer Top_printers.ppgenarginfo
+install_printer Top_printers.ppgenargargt
+install_printer Top_printers.ppist
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 44d44ccc4b..fd08f9ffe8 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -168,8 +168,8 @@ let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n)
 (* proof printers *)
 let pr_evar ev = Pp.int (Evar.repr ev)
 let ppmetas metas = pp(Termops.pr_metaset metas)
-let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes (Some 2) evd)
-let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None evd)
+let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes (Some 2) (Global.env ()) evd)
+let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None (Global.env ()) evd)
 let pr_existentialset evars =
   prlist_with_sep spc pr_evar (Evar.Set.elements evars)
 let ppexistentialset evars =
@@ -180,14 +180,14 @@ let ppexistentialfilter filter = match Evd.Filter.repr filter with
 let ppclenv clenv = pp(pr_clenv clenv)
 let ppgoalgoal gl = pp(Goal.pr_goal gl)
 let ppgoal g = pp(Printer.pr_goal g)
-let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Refiner.project g))
+let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Global.env ()) (Refiner.project g))
 let pphintdb db = pp(envpp Hints.pr_hint_db_env db)
 let ppproofview p =
   let gls,sigma = Proofview.proofview p in
-  pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) sigma)
+  pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) (Global.env ()) sigma)
 
 let ppopenconstr (x : Evd.open_constr) =
-  let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_econstr_env c)
+  let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) (Global.env ()) evd ++ envpp pr_econstr_env c)
 (* spiwack: deactivated until a replacement is found
 let pppftreestate p = pp(print_pftreestate p)
 *)