9 files changed, 81 insertions, 49 deletions
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/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 50d4d21637..f422030b53 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -238,7 +238,7 @@
 ########################################################################
 # plugin_tutorial
 ########################################################################
-: "${plugin_tutorial_CI_REF:=master}"
+: "${plugin_tutorial_CI_REF:=14b2976cdf67db788b79d9421ce1e89bd15c7313}"
 : "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}"
 : "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}"
 
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 58bbb7229f..60436e672c 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -8,11 +8,6 @@ wget -qO- "${sf_lf_CI_TARURL}"  | tar xvz
 wget -qO- "${sf_plf_CI_TARURL}" | tar xvz
 wget -qO- "${sf_vfa_CI_TARURL}" | tar xvz
 
-sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v
-sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v
-
-( cd lf && make clean && make )
-
-( cd plf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make )
-
+( cd lf  && make clean && make )
+( cd plf && make clean && make )
 ( cd vfa && make clean && make )
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/08704-ejgallego-vernac+monify_hook.sh b/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh
new file mode 100644
index 0000000000..b3a9f67e00
--- /dev/null
+++ b/dev/ci/user-overlays/08704-ejgallego-vernac+monify_hook.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "8704" ] || [ "$CI_BRANCH" = "vernac+monify_hook" ]; then
+
+    # ltac2_CI_REF=rm-section-path
+    # ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+    plugin_tutorial_CI_REF=vernac+monify_hook
+    plugin_tutorial_CI_GITURL=https://github.com/ejgallego/plugin_tutorials
+
+    Elpi_CI_REF=vernac+monify_hook
+    Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+    Equations_CI_REF=vernac+monify_hook
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
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/changes.md b/dev/doc/changes.md
index 40013712fd..eb5b9ee1d3 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -19,6 +19,19 @@ Names
   Constant.make3 has been removed, use Constant.make2
   Constant.repr3 has been removed, use Constant.repr2
 
+Coqlib:
+
+- Most functions from the `Coqlib` module have been deprecated in favor of
+  `register_ref` and `lib_ref`. The first one is available through the
+  vernacular `Register` command; it binds a name to a constant. The second
+  command then enables to locate the registered constant through its name. The
+  name resolution is dynamic.
+
+Macros:
+
+- The RAW_TYPED AS and GLOB_TYPED AS stanzas of the ARGUMENT EXTEND macro are
+  deprecated. Use TYPED AS instead.
+
 ## Changes between Coq 8.8 and Coq 8.9
 
 ### ML API
@@ -201,7 +214,48 @@ END
 
 #### ARGUMENT EXTEND
 
-Not handled yet.
+Steps to perform:
+- replace the brackets enclosing OCaml code in actions with braces
+- if not there yet, add a leading `|` to the first rule
+- syntax of `TYPED AS` has been restricted not to accept compound generic
+  arguments as a literal, e.g. `foo_opt` should be rewritten into `foo option`
+  and similarly `foo_list` into `foo list`.
+- parenthesis around pair types in `TYPED AS` are now mandatory
+- `RAW_TYPED AS` and `GLOB_TYPED AS` clauses need to be removed
+
+`BY` clauses are considered OCaml code, and thus need to be wrapped in braces,
+but not the `TYPED AS` clauses.
+
+For instance, code of the form:
+```
+ARGUMENT EXTEND my_arg
+  TYPED AS int_opt
+  PRINTED BY printer
+  INTERPRETED BY interp_f
+  GLOBALIZED BY glob_f
+  SUBSTITUTED BY subst_f
+  RAW_TYPED AS int_opt
+  RAW_PRINTED BY raw_printer
+  GLOB_TYPED AS int_opt
+  GLOB_PRINTED BY glob_printer
+  [ "foo" int(i) ] -> [ my_arg1 i ]
+| [ "bar" ] -> [ my_arg2 ]
+END
+```
+should be turned into
+```
+ARGUMENT EXTEND my_arg
+  TYPED AS { int_opt }
+  PRINTED BY { printer }
+  INTERPRETED BY { interp_f }
+  GLOBALIZED BY { glob_f }
+  SUBSTITUTED BY { subst_f }
+  RAW_PRINTED BY { raw_printer }
+  GLOB_PRINTED BY { glob_printer }
+| [ "foo" int(i) ] -> { my_arg1 i }
+| [ "bar" ] -> { my_arg2 }
+END
+```
 
 #### GEXTEND
 
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-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)))