17 files changed, 300 insertions, 47 deletions
diff --git a/dev/base_include b/dev/base_include
index 2f5d8aa843..fc38305cca 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -189,7 +189,7 @@ let qid = Libnames.qualid_of_string;;
 (* parsing of terms *)
 
 let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
-let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac_control;;
+let parse_vernac = Pcoq.parse_string Pvernac.Vernac_.vernac_control;;
 let parse_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
@@ -204,7 +204,9 @@ let e s =
    implicit syntax *)
 
 let constr_of_string s = 
-  Constrintern.interp_constr (Global.env()) Evd.empty (parse_constr s);;
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  Constrintern.interp_constr env sigma (parse_constr s);;
 
 (* get the body of a constant *)
 
diff --git a/dev/ci/README.md b/dev/ci/README.md
index ed3442e0db..697a160ca9 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -107,19 +107,32 @@ there are some.
 
 You can also run one CI target locally (using `make ci-somedev`).
 
-Whenever your PR breaks tested developments, you should either adapt it
-so that it doesn't, or provide a branch fixing these developments (or at
-least work with the author of the development / other Coq developers to
-prepare these fixes). Then, add an overlay in
-[`dev/ci/user-overlays`](/dev/ci/user-overlays) (see the README there)
-as part of your PR.
-
-The process to merge your PR is then to submit PRs to the external
-development repositories, merge the latter first (if the fixes are
-backward-compatible), and merge the PR on Coq then.
-
 See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite.
 
+### Breaking changes
+
+When your PR breaks an external project we test in our CI, you must prepare a
+patch (or ask someone to prepare a patch) to fix the project:
+
+1. Fork the external project, create a new branch, push a commit adapting
+   the project to your changes.
+2. Test your pull request with your adapted version of the external project by
+   adding an overlay file to your pull request (cf.
+   [`dev/ci/user-overlays/README.md`](/dev/ci/user-overlays/README.md)).
+3. Fixes to external libraries (pure Coq projects) *must* be backward
+   compatible (i.e. they should also work with the development version of Coq,
+   and the latest stable version). This will allow you to open a PR on the
+   external project repository to have your changes merged *before* your PR on
+   Coq can be integrated.
+
+   On the other hand, patches to plugins (projects linking to the Coq ML API)
+   can very rarely be made backward compatible and plugins we test will
+   generally have a dedicated branch per Coq version.
+   You can still open a pull request but the merging will be requested by the
+   developer who merges the PR on Coq. There are plans to improve this, cf.
+   [#6724](https://github.com/coq/coq/issues/6724).
+
+Moreover your PR must absolutely update the [`CHANGES`](/CHANGES) file.
 
 Advanced GitLab CI information
 ------------------------------
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 5c882ee856..87d837b387 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -170,3 +170,15 @@
 ########################################################################
 : "${pidetop_CI_BRANCH:=v8.9}"
 : "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop.git}"
+
+########################################################################
+# ext-lib
+########################################################################
+: "${ext_lib_CI_BRANCH:=master}"
+: "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib.git}"
+
+########################################################################
+# quickchick
+########################################################################
+: "${quickchick_CI_BRANCH:=master}"
+: "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick.git}"
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index f867fd189b..5b5cbd11ae 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -8,6 +8,7 @@ export NJOBS
 
 if [ -n "${GITLAB_CI}" ];
 then
+    export OCAMLPATH="$PWD/_install_ci/lib:$OCAMLPATH"
     export COQBIN="$PWD/_install_ci/bin"
     export CI_BRANCH="$CI_COMMIT_REF_NAME"
     if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]
@@ -27,6 +28,7 @@ else
         CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
         export CI_BRANCH
     fi
+    export OCAMLPATH="$PWD:$OCAMLPATH"
     export COQBIN="$PWD/bin"
 fi
 export PATH="$COQBIN:$PATH"
diff --git a/dev/ci/ci-ext-lib.sh b/dev/ci/ci-ext-lib.sh
new file mode 100755
index 0000000000..cf212c2fb5
--- /dev/null
+++ b/dev/ci/ci-ext-lib.sh
@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+
+# This script could be included inside other ones
+# Let's avoid to source ci-common twice in this case
+if [ -z "${CI_BUILD_DIR}" ];
+then
+    . "${ci_dir}/ci-common.sh"
+fi
+
+ext_lib_CI_DIR="${CI_BUILD_DIR}/ExtLib"
+
+git_checkout "${ext_lib_CI_BRANCH}" "${ext_lib_CI_GITURL}" "${ext_lib_CI_DIR}"
+
+( cd "${ext_lib_CI_DIR}" && make && make install)
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 5d96c24991..48a1366aba 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 -j 1 ${fiat_crypto_CI_TARGETS2} )
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
index 2ac4d21671..32cba0808e 100755
--- a/dev/ci/ci-pidetop.sh
+++ b/dev/ci/ci-pidetop.sh
@@ -12,13 +12,11 @@ git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}"
 # `-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
-   COQOCAMLLIB="$COQBIN/../lib/"
    COQLIB="$COQBIN/../lib/coq/"
 else
-   COQOCAMLLIB="$COQBIN/../"
    COQLIB="$COQBIN/../"
 fi
 
-( cd "${pidetop_CI_DIR}" && OCAMLPATH="$COQOCAMLLIB" jbuilder build @install )
+( cd "${pidetop_CI_DIR}" && jbuilder build @install )
 
 echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds
diff --git a/dev/ci/ci-quickchick.sh b/dev/ci/ci-quickchick.sh
new file mode 100755
index 0000000000..fc39e2685d
--- /dev/null
+++ b/dev/ci/ci-quickchick.sh
@@ -0,0 +1,18 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+
+# This script could be included inside other ones
+# Let's avoid to source ci-common twice in this case
+if [ -z "${CI_BUILD_DIR}" ];
+then
+    . "${ci_dir}/ci-common.sh"
+fi
+
+quickchick_CI_DIR="${CI_BUILD_DIR}/Quickchick"
+
+install_ssreflect
+
+git_checkout "${quickchick_CI_BRANCH}" "${quickchick_CI_GITURL}" "${quickchick_CI_DIR}"
+
+( cd "${quickchick_CI_DIR}" && make && make install)
diff --git a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh
index ca0076b468..b22ab36302 100644
--- a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh
+++ b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh
@@ -1,6 +1,9 @@
 #!/bin/sh
 
-if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top" ] || [ "$CI_BRANCH" = "pr-6859" ]; then
+if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top"   ] ||     \
+   [ "$CI_PULL_REQUEST" = "7543" ] || [ "$CI_BRANCH" = "ide+split" ] ; then
+
     pidetop_CI_BRANCH=stm+top
     pidetop_CI_GITURL=https://bitbucket.org/ejgallego/pidetop.git
+
 fi
diff --git a/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh
new file mode 100644
index 0000000000..ea9cd8ee07
--- /dev/null
+++ b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh
@@ -0,0 +1,21 @@
+if [ "$CI_PULL_REQUEST" = "7196" ] || [ "$CI_BRANCH" = "tactics+push_fix_naming_out" ] || [ "$CI_BRANCH" = "pr-7196" ]; then
+
+    # Needed overlays: https://gitlab.com/coq/coq/pipelines/21244550
+    #
+    # equations
+    # ltac2
+
+    # The below developments should instead use a backwards compatible fix.
+    #
+    # color
+    # iris-lambda-rust
+    # math-classes
+    # formal-topology
+
+    ltac2_CI_BRANCH=tactics+push_fix_naming_out
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+    Equations_CI_BRANCH=tactics+push_fix_naming_out
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh b/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh
new file mode 100644
index 0000000000..115f29f1ee
--- /dev/null
+++ b/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh
@@ -0,0 +1,14 @@
+if [ "$CI_PULL_REQUEST" = "7558" ] || [ "$CI_BRANCH" = "vernac+move_parser" ]; then
+
+    _OVERLAY_BRANCH=vernac+move_parser
+
+    Equations_CI_BRANCH="$_OVERLAY_BRANCH"
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    ltac2_CI_BRANCH="$_OVERLAY_BRANCH"
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+    mtac2_CI_BRANCH="$_OVERLAY_BRANCH"
+    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index a7474e3248..aec2dfe0a6 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -1,8 +1,21 @@
 # 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).
+When your pull request breaks an external project we test in our CI and you
+have prepared a branch with the fix, you can add an "overlay" to your pull
+request to test it with the adapted version of the external project.
 
-The name of your overlay file should be of the form `five_digit_PR_number-GitHub_handle-branch_name.sh`.
+An overlay is a file which defines where to look for the patched version so that
+testing is possible. It redefines some variables from
+[`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh):
+give the name of your branch using a `_CI_BRANCH` variable and the location of
+your fork using a `_CI_GITURL` variable.
+
+Moreover, the file contains very simple logic to test the pull request number
+or branch name and apply it only in this case.
+
+The name of your overlay file should start with a five-digit pull request
+number, followed by a dash, anything (for instance your GitHub nickname
+and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`).
 
 Example: `00669-maximedenes-ssr-merge.sh` containing
 
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index a466124c1c..65457b63af 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -1,8 +1,8 @@
 # Merging changes in Coq
 
-This document describes how patches (submitted as pull requests
-on the `master` branch) should be
-merged into the main repository (https://github.com/coq/coq).
+This document describes how patches, submitted as pull requests (PRs) on the
+`master` branch, should be merged into the main repository
+(https://github.com/coq/coq).
 
 ## Code owners
 
@@ -10,8 +10,8 @@ The [CODEOWNERS](/.github/CODEOWNERS) file describes, for each part of the
 system, two owners. One is the principal maintainer of the component, the other
 is the secondary maintainer.
 
-When a pull request is submitted, GitHub will automatically ask the principal
-maintainer for a review. If the pull request touches several parts, all the
+When a PR is submitted, GitHub will automatically ask the principal
+maintainer for a review. If the PR touches several parts, all the
 corresponding principal maintainers will be asked for a review.
 
 Maintainers are never assigned as reviewer on their own PRs.
@@ -43,10 +43,31 @@ A maintainer is expected to be reasonably reactive, but no specific timeframe is
 given for reviewing.
 
 (*) In case a component is touched in a trivial way (adding/removing one file in
-a `Makefile`, etc), or by applying a systematic process (global renaming,
-deprecationg propagation, etc) that has been reviewed globally, the assignee can
+a `Makefile`, etc), or by applying a systematic refactoring process (global
+renaming for instance) that has been reviewed globally, the assignee can
 say in a comment they think a review is not required and proceed with the merge.
 
+### Breaking changes
+
+If the PR breaks compatibility of some external projects in CI, then fixes to
+those external projects should have been prepared (cf. the relevant sub-section
+in the [CI README](/dev/ci/README.md#Breaking-changes) and the PR can be tested
+with these fixes thanks to ["overlays"](/dev/ci/user-overlays/README.md).
+
+Moreover the PR must absolutely update the [`CHANGES`](/CHANGES) file.
+
+If overlays are missing, ask the author to prepare them and label the PR with
+the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label.
+
+When fixes are ready, there are two cases to consider:
+
+- For patches that are backward compatible (best scenario), you should get the
+  external project maintainers to integrate them before merging the PR.
+- For patches that are not backward compatible (which is often the case when
+  patching plugins after an update to the Coq API), you can proceed to merge
+  the PR and then notify the external project maintainers they can merge the
+  patch.
+
 ## Merging
 
 Once all reviewers approved the PR, the assignee is expected to check that CI
@@ -89,22 +110,6 @@ DON'T USE the GitHub interface for merging, since it will prevent the automated
 backport script from operating properly, generates bad commit messages, and a
 messy history when there are conflicts.
 
-### What to do if the PR has overlays
-
-If the PR breaks compatibility of some developments in CI, then the author must
-have prepared overlays for these developments (see [`dev/ci/README.md`](/dev/ci/README.md))
-and the PR must absolutely update the `CHANGES` file.
-
-There are two cases to consider:
-
-- If the patch is backward compatible (best scenario), then you should get
-  upstream maintainers to integrate it before merging the PR.
-- If the patch is not backward compatible (which is often the case when
-  patching plugins after an update to the Coq API), then you can proceed to
-  merge the PR and then notify upstream they can merge the patch. This is a
-  less preferable scenario because it is probably going to create
-  spurious CI failures for unrelated PRs.
-
 ### Merge script dependencies
 
 The merge script passes option `-S` to `git merge` to ensure merge commits
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index ff448abe81..4838dd734a 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -4,7 +4,7 @@
 
 Misctypes
 
-  Syntax for universe sorts and kinds has been moved from `Misctypes`
+- Syntax for universe sorts and kinds has been moved from `Misctypes`
   to `Glob_term`, as these are turned into kernel terms by
   `Pretyping`.
 
@@ -28,6 +28,38 @@ Proof engine
   should indicate what the canonical form is. An important change is
   the move of `Globnames.global_reference` to `Names.GlobRef.t`.
 
+ML Libraries used by Coq
+
+- Introduction of a "Smart" module for collecting "smart*" functions, e.g.
+  Array.Smart.map.
+- Uniformization of some names, e.g. Array.Smart.fold_left_map instead
+  of Array.smartfoldmap.
+
+Printer.ml API
+
+- The mechanism in Printer that allowed dynamically overriding pr_subgoals,
+  pr_subgoal and pr_goal was removed to simplify the code.  It was
+  earlierly used by PCoq.
+
+Source code organization
+
+- We have eliminated / fused some redundant modules and relocated a
+  few interfaces files. The `intf` folder is gone, and now for example
+  `Constrexpr` is located in `interp/`, `Vernacexpr` in `vernac/` and
+  so on. Changes should be compatible, but in a few cases stricter
+  layering requirements may mean that functions have moved. In all
+  cases adapting is a matter of changing the module name.
+
+Vernacular commands
+
+- The implementation of vernacular commands has been refactored so it
+  is self-contained now, including the parsing and extension
+  mechanisms. This involves a couple of non-backward compatible
+  changes due to layering issues, where some functions have been moved
+  from `Pcoq` to `Pvernac` and from `Vernacexpr` to modules in
+  `tactics/`. In all cases adapting is a matter of changing the module
+  name.
+
 ### Unit testing
 
   The test suite now allows writing unit tests against OCaml code in the Coq
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
new file mode 100644
index 0000000000..1821a181f1
--- /dev/null
+++ b/dev/doc/release-process.md
@@ -0,0 +1,100 @@
+# Release process #
+
+## As soon as the previous version branched off master ##
+
+- [ ] Create a new issue to track the release process where you can copy-paste
+  the present checklist.
+- [ ] Change the version name to the next major version and the magic numbers
+  (see [#7008](https://github.com/coq/coq/pull/7008/files)).
+- [ ] Put the corresponding alpha tag using `git tag -s`.
+  The `VX.X+alpha` tag marks the first commit to be in `master` and not in the
+  branch of the previous version.
+- [ ] Create the `X.X+beta1` milestone if it did not already exist.
+- [ ] Decide the release calendar with the team (freeze date, beta date, final
+  release date) and put this information in the milestone (using the
+  description and due date fields).
+
+## About one month before the beta ##
+
+- [ ] Create the `X.X.0` milestone and set its due date.
+- [ ] Send an announcement of the upcoming freeze on Coqdev and ask people to
+  remove from the beta milestone what they already know won't be ready on time
+  (possibly postponing to the `X.X.0` milestone for minor bug fixes,
+  infrastructure and documentation updates).
+- [ ] Determine which issues should / must be fixed before the beta, add them
+  to the beta milestone, possibly with a
+  ["priority: blocker"](https://github.com/coq/coq/labels/priority%3A%20blocker)
+  label. Make sure that all these issues are assigned (and that the assignee
+  provides an ETA).
+- [ ] Ping the development coordinator (**@mattam82**) to get him started on
+  the update to the Credits chapter of the reference manual.
+  See also [#7058](https://github.com/coq/coq/issues/7058).
+  The command to get the list of contributors for this version is
+  `git shortlog -s -n VX.X+alpha..master | cut -f2 | sort -k 2`
+  (the ordering is approximative as it will misplace people with middle names).
+
+## On the date of the feature freeze ##
+
+- [ ] Create the new version branch `vX.X` and
+  [protect it](https://github.com/coq/coq/settings/branches)
+  (activate the "Protect this branch", "Require pull request reviews before
+  merging" and "Restrict who can push to this branch" guards).
+- [ ] Remove all remaining unmerged feature PRs from the beta milestone.
+- [ ] Start a new project to track PR backporting. The proposed model is to
+  have a "X.X-only PRs" column for the rare PRs on the stable branch, a
+  "Request X.X inclusion" column for the PRs that were merged in `master` that
+  are to be considered for backporting, a "Waiting for CI" column to put the
+  PRs in the process of being backported, and "Shipped in ..." columns to put
+  what was backported. (The release manager is the person responsible for
+  merging PRs that target the version branch and backporting appropriate PRs
+  that are merged into `master`).
+  A message to **@coqbot** in the milestone description tells it to
+  automatically add merged PRs to the "Request X.X inclusion" column.
+- [ ] Delay non-blocking issues to the appropriate milestone and ensure
+  blocking issues are solved. If required to solve some blocking issues,
+  it is possible to revert some feature PRs in the version branch only.
+
+## Before the beta release date ##
+
+- [ ] Ensure the Credits chapter has been updated.
+- [ ] Ensure an empty `CompatXX.v` file has been created.
+- [ ] Ensure that an appropriate version of the plugins we will distribute with
+  Coq has been tagged.
+- [ ] Have some people test the recently auto-generated Windows and MacOS
+  packages.
+- [ ] Change the version name from alpha to beta1 (see
+  [#7009](https://github.com/coq/coq/pull/7009/files)).
+  We generally do not update the magic numbers at this point.
+- [ ] Put the `VX.X+beta1` tag using `git tag -s`.
+
+### These steps are the same for all releases (beta, final, patch-level) ###
+
+- [ ] Send an e-mail on Coqdev announcing that the tag has been put so that
+  package managers can start preparing package updates.
+- [ ] Draft a release on GitHub.
+- [ ] Get **@maximedenes** to sign the Windows and MacOS packages and
+  upload them on GitHub.
+- [ ] Prepare a page of news on the website with the link to the GitHub release
+  (see [coq/www#63](https://github.com/coq/www/pull/63)).
+- [ ] Upload the new version of the reference manual to the website.
+  *TODO: setup some continuous deployment for this.*
+- [ ] Merge the website update, publish the release
+  and send annoucement e-mails.
+- [ ] Ping **@Zimmi48** to publish a new version on Zenodo.
+  *TODO: automate this.*
+- [ ] Close the milestone
+
+## At the final release time ##
+
+- [ ] Change the version name to X.X.0 and the magic numbers (see
+  [#7271](https://github.com/coq/coq/pull/7271/files)).
+- [ ] Put the `VX.X.0` tag.
+
+Repeat the generic process documented above for all releases.
+
+- [ ] Switch the default version of the reference manual on the website.
+
+## At the patch-level release time ##
+
+We generally do not update the magic numbers at this point (see
+[`2881a18`](https://github.com/coq/coq/commit/2881a18)).
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index cb1abc4a94..10a7a4158b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -221,7 +221,9 @@ let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c)
 let ppabstract_cumulativity_info c = pp (Univ.pr_abstract_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))
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  pp (pr_named_context env sigma (named_context_of_val e))
 
 let ppenv e = pp
   (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
@@ -230,7 +232,7 @@ let ppenv e = pp
 let ppenvwithcst e = pp
   (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
    str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++
-   str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}")
+   str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).env_globals.env_constants (mt ()) ++ str "}")
 
 let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x))
 
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 2ddf927d9b..16917586f5 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -1,5 +1,6 @@
 open Format
 open Term
+open Constr
 open Names
 open Cbytecodes
 open Cemitcodes