8 files changed, 25 insertions, 20 deletions
diff --git a/dev/base_include b/dev/base_include
index d2e8f6d092..48feeec147 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -8,6 +8,7 @@
 #directory "toplevel";;
 #directory "library";;
 #directory "kernel";;
+#directory "gramlib";;
 #directory "engine";;
 #directory "pretyping";;
 #directory "lib";;
@@ -18,8 +19,6 @@
 #directory "stm";;
 #directory "vernac";;
 
-#directory "+camlp5";; (* Gramext is found in top_printers.ml *)
-
 #use "top_printers.ml";;
 #use "vm_printers.ml";;
 
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 0dcabc0b97..d0b5f4be47 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1076,7 +1076,7 @@ function make_ocaml {
 
 function make_ocaml_tools {
   make_findlib
-  make_camlp5
+  # make_camlp5
 }
 
 ##### OCAML EXTRA LIBRARIES #####
@@ -1386,7 +1386,7 @@ function make_coq {
   make_ocaml
   make_num
   make_findlib
-  make_camlp5
+  # make_camlp5
   make_lablgtk
   if
     case $COQ_VERSION in
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 7ed90f524c..bc49e3e76b 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -84,10 +84,10 @@ unless these tests pass.
 
 We are currently running tests on the following platforms:
 
-- GitLab CI is the main CI platform. It tests the compilation of Coq, of the
-  documentation, and of CoqIDE on Linux with several versions of OCaml /
-  camlp5, and with warnings as errors; it runs the test-suite and tests the
-  compilation of several external developments.
+- GitLab CI is the main CI platform. It tests the compilation of Coq,
+  of the documentation, and of CoqIDE on Linux with several versions
+  of OCaml and with warnings as errors; it runs the test-suite and
+  tests the compilation of several external developments.
 
 - Travis CI is used to test the compilation of Coq and run the test-suite on
   macOS. It also runs a linter that checks whitespace discipline. A
diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh
index 84fec71f7a..abeb039c0e 100644
--- a/dev/ci/appveyor.sh
+++ b/dev/ci/appveyor.sh
@@ -10,6 +10,6 @@ bash opam64/install.sh
 
 opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $APPVEYOR_OPAM_SWITCH --switch $APPVEYOR_OPAM_SWITCH
 eval "$(opam config env)"
-opam install -y num ocamlfind camlp5 ounit
+opam install -y num ocamlfind ounit
 
 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 4ddb582414..3fc6dce4e5 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-10-30-V1"
+# CACHEKEY: "bionic_coq-V2018-11-08-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -41,29 +41,27 @@ 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.
-ENV CAMLP5_VER="7.03" \
-    COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
+ENV COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
 
 # base switch
 RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \
-    opam install $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM
+    opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM
 
 # base+32bit switch
 RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
-    opam install $BASE_OPAM camlp5.$CAMLP5_VER
+    opam install $BASE_OPAM
 
 # EDGE switch
 ENV COMPILER_EDGE="4.07.1" \
-    CAMLP5_VER_EDGE="7.06.10-g84ce6cc4" \
     COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \
     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
+    opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
 RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \
-    opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM
+    opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE $CI_OPAM
 
 RUN opam clean -a -c
diff --git a/dev/doc/README.md b/dev/doc/README.md
index 223cf6286e..c764455aed 100644
--- a/dev/doc/README.md
+++ b/dev/doc/README.md
@@ -16,7 +16,6 @@ $ opam init --comp <latest-ocaml-version>
   ~/.bashrc and ~/.ocamlinit files.
 
 $ source ~/.bashrc
-$ opam install camlp5
 
 # needed if you want to build "coqide" target
 
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 30a2967259..acb0d80c18 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,5 +1,15 @@
 ## Changes between Coq 8.9 and Coq 8.10
 
+### ML4 Pre Processing
+
+- Support for `.ml4` files, processed by camlp5 has been removed in
+  favor of `.mlg` files processed by `coqpp`.
+
+  Porting is usually straightforward, and involves renaming the
+  `file.ml4` file to `file.mlg` and adding a few brackets.
+
+  See "Transitioning away from Camlp5" below for update instructions.
+
 ### ML API
 
 General deprecation
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index d330f517be..707c7f07ce 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -8,14 +8,13 @@
 # here are some reasonable default values
 
 [ -z "$OCAMLDEBUG" ] && OCAMLDEBUG=ocamldebug
-[ -z "$CAMLP5LIB" ] && CAMLP5LIB=+camlp5
 [ -z "$COQTOP" -a -d "$PWD/kernel" ] && COQTOP=$PWD
 [ -z "$COQTOP" -a -d "$PWD/../kernel" ] && COQTOP=`dirname $PWD`
 
 export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH
 
 exec $OCAMLDEBUG \
-    -I $CAMLP5LIB -I +threads \
+    -I +threads \
     -I $COQTOP \
     -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
     -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \