13 files changed, 203 insertions, 10 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/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 feabf72d48..48a1366aba 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -11,4 +11,4 @@ git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypt
 
 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} )
+( 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/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/doc/changes.md b/dev/doc/changes.md
index 774a77c8ad..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`.
 
@@ -35,6 +35,31 @@ ML Libraries used by Coq
 - 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