10 files changed, 86 insertions, 6 deletions
diff --git a/dev/base_include b/dev/base_include
index 8d81ca3e04..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 
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-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/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 cd28b1b50f..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`.
 
@@ -41,6 +41,25 @@ Printer.ml API
   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/top_printers.ml b/dev/top_printers.ml
index 129f171b2a..10a7a4158b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -232,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