9 files changed, 50 insertions, 34 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 94e90bf4f..da5ac2b15 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -793,7 +793,7 @@ function make_ln {
 
 function make_ocaml {
   get_flex_dll_link_bin
-  if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.06 ocaml-4.06.1 tar.gz 1 ; then
+  if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.07 ocaml-4.07.0 tar.gz 1 ; then
     # See README.win32.adoc
     cp config/m-nt.h byterun/caml/m.h
     cp config/s-nt.h byterun/caml/s.h
@@ -933,7 +933,7 @@ function make_camlp5 {
   make_ocaml
   make_findlib
 
-  if build_prep https://github.com/camlp5/camlp5/archive rel705 tar.gz 1 camlp5-rel705; then
+  if build_prep https://github.com/camlp5/camlp5/archive rel706 tar.gz 1 camlp5-rel706; then
     logn configure ./configure
     # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success
     sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile
diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh
index 7bf9ad8c9..d2176e326 100644
--- a/dev/ci/appveyor.sh
+++ b/dev/ci/appveyor.sh
@@ -2,7 +2,7 @@
 
 set -e -x
 
-APPVEYOR_OPAM_SWITCH=4.06.1+mingw64c
+APPVEYOR_OPAM_SWITCH=4.07.0+mingw64c
 
 wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/opam64.tar.xz
 tar -xf opam64.tar.xz
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index a4ee6a379..1361392dc 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-07-02-V4"
+# CACHEKEY: "bionic_coq-V2018-07-11-V2"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -28,7 +28,7 @@ RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml.
 # 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 jbuilder.1.0+beta20 ounit.2.0.8" \
+ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.0.0 ounit.2.0.8" \
     CI_OPAM="menhir.20180530 elpi.1.0.4 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
@@ -43,8 +43,8 @@ RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \
     opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER
 
 # EDGE switch
-ENV COMPILER_EDGE="4.06.1" \
-    CAMLP5_VER_EDGE="7.05" \
+ENV COMPILER_EDGE="4.07.0" \
+    CAMLP5_VER_EDGE="7.06" \
     COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2"
 
 RUN opam switch -y -j $NJOBS $COMPILER_EDGE && eval $(opam config env) && \
diff --git a/dev/ci/user-overlays/07746-cleanup-unused-various.sh b/dev/ci/user-overlays/07746-cleanup-unused-various.sh
deleted file mode 100644
index 8688b0d53..000000000
--- a/dev/ci/user-overlays/07746-cleanup-unused-various.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/bin/sh
-
-if [ "$CI_PULL_REQUEST" = "7746" ] || [ "$CI_BRANCH" = "cleanup-unused-various" ]; then
-    Equations_CI_BRANCH="adapt-unused"
-    Equations_CI_GITURL="https://github.com/SkySkimmer/Coq-Equations.git"
-fi
diff --git a/dev/ci/user-overlays/07820-mattam82-hints-constants.sh b/dev/ci/user-overlays/07820-mattam82-hints-constants.sh
deleted file mode 100644
index 2ae86ae22..000000000
--- a/dev/ci/user-overlays/07820-mattam82-hints-constants.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-_OVERLAY_BRANCH=hints-variables-overlay
-
-if [ "$CI_PULL_REQUEST" = "7820" ] || [ "$CI_BRANCH" = "_OVERLAY_BRANCH" ]; then
-
-    Equations_CI_BRANCH="$_OVERLAY_BRANCH"
-fi
diff --git a/dev/ci/user-overlays/07902-ppedrot-camlp5-parser.sh b/dev/ci/user-overlays/07902-ppedrot-camlp5-parser.sh
deleted file mode 100644
index 735153ebd..000000000
--- a/dev/ci/user-overlays/07902-ppedrot-camlp5-parser.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-_OVERLAY_BRANCH=camlp5-parser
-
-if [ "$CI_PULL_REQUEST" = "7902" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
-
-    ltac2_CI_BRANCH="$_OVERLAY_BRANCH"
-    ltac2_CI_GITURL=https://github.com/ppedrot/ltac2
-
-fi
diff --git a/dev/doc/README.md b/dev/doc/README.md
index 1a4e40f68..223cf6286 100644
--- a/dev/doc/README.md
+++ b/dev/doc/README.md
@@ -7,7 +7,7 @@ Assuming one is running Ubuntu (if not, replace `apt` with the package manager o
 ```
 $ sudo apt-get install make opam git
 
-# At the time of writing, <latest-ocaml-version> is 4.06.1.
+# At the time of writing, <latest-ocaml-version> is 4.07.0.
 # The latest version number is available at: https://ocaml.org/releases/
 
 $ opam init --comp <latest-ocaml-version>
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 6d5023405..1eea2443f 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -88,6 +88,11 @@ Primitive number parsers
   have been split over three files (plugins/syntax/positive_syntax.ml,
   plugins/syntax/n_syntax.ml, plugins/syntax/z_syntax.ml).
 
+Parsing
+
+- Manual uses of the Pcoq.Gram module have been deprecated. Wrapper modules
+  Pcoq.Entry and Pcoq.Parsable were introduced to replace it.
+
 ### Unit testing
 
   The test suite now allows writing unit tests against OCaml code in the Coq
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index 5205350a6..9864fd4d6 100755
--- a/dev/tools/backport-pr.sh
+++ b/dev/tools/backport-pr.sh
@@ -1,11 +1,34 @@
 #!/usr/bin/env bash
 
-# Usage: dev/tools/backport-pr.sh <PR number> [--stop-before-merging]
-
 set -e
 
-PRNUM=$1
-OPTION=$2
+if [[ $# == 0 ]]; then
+    echo "Usage: $0 [--no-conflict] [--no-signature-check] [--stop-before-merging] prnum"
+    exit 1
+fi
+
+while [[ $# -gt 0 ]]; do
+    case "$1" in
+        --no-conflict)
+            NO_CONFLICTS="true"
+            shift
+            ;;
+        --no-signature-check)
+            NO_SIGNATURE_CHECK="true"
+            shift
+            ;;
+        --stop-before-merging)
+            STOP_BEFORE_MERGING="true"
+            shift
+            ;;
+        *)
+            if [[ "$PRNUM" != "" ]]; then
+                echo "PRNUM was already set to $PRNUM and is now being overridden with $1."
+            fi
+            PRNUM="$1"
+            shift
+    esac
+done
 
 if ! git log master --grep "Merge PR #${PRNUM}" | grep "." > /dev/null; then
     echo "PR #${PRNUM} does not exist."
@@ -14,7 +37,7 @@ fi
 
 SIGNATURE_STATUS=$(git log master --grep "Merge PR #${PRNUM}" --format="%G?")
 git log master --grep "Merge PR #${PRNUM}" --format="%GG"
-if [[ "${SIGNATURE_STATUS}" != "G" ]]; then
+if [[ "$NO_SIGNATURE_CHECK" != "true" && "$SIGNATURE_STATUS" != "G" ]]; then
     echo
     read -p "Merge commit does not have a good (valid) signature. Bypass? [y/N] " -n 1 -r
     echo
@@ -30,6 +53,14 @@ MESSAGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%s" | sed 's/Merg
 if git checkout -b "${BRANCH}"; then
 
     if ! git cherry-pick -x "${RANGE}"; then
+        if [[ "$NO_CONFLICTS" == "true" ]]; then
+            git status
+            echo "Conflicts! Aborting..."
+            git cherry-pick --abort
+            git checkout -
+            git branch -d "$BRANCH"
+            exit 1
+        fi
         echo "Please fix the conflicts, then exit."
         bash
         while ! git cherry-pick --continue; do
@@ -59,7 +90,7 @@ if ! git diff --exit-code HEAD "${BRANCH}" -- "*.mli"; then
     fi
 fi
 
-if [[ "${OPTION}" == "--stop-before-merging" ]]; then
+if [[ "$STOP_BEFORE_MERGING" == "true" ]]; then
     exit 0
 fi