4 files changed, 77 insertions, 18 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 85df249d3..a68cd0933 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -69,7 +69,7 @@ git_checkout()
     if [ ! -d .git ] ; then git clone "${_DEPTH[@]}" "${_URL}" . ; fi && \
     echo "Checking out ${_DEST}"                                      && \
     git fetch "${_URL}" "${_BRANCH}"                                  && \
-    git checkout "${_COMMIT}"                                         && \
+    git -c advice.detachedHead=false checkout "${_COMMIT}"            && \
     echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" )
 }
 
diff --git a/dev/ci/user-overlays/07746-cleanup-unused-various.sh b/dev/ci/user-overlays/07746-cleanup-unused-various.sh
new file mode 100644
index 000000000..8688b0d53
--- /dev/null
+++ b/dev/ci/user-overlays/07746-cleanup-unused-various.sh
@@ -0,0 +1,6 @@
+#!/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/doc/changes.md b/dev/doc/changes.md
index 4177513a1..6d5023405 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -95,19 +95,73 @@ Primitive number parsers
 
 ### Transitioning away from Camlp5
 
-In an effort to reduce dependency on Camlp5, the use of Camlp5 GEXTEND macro
-is discouraged. Most plugin writers do not need this low-level interface, but
-for those who do, the transition path is somewhat straightforward. To convert
-a ml4 file containing only standard OCaml with GEXTEND statements, the following
-should be enough:
-- replace its "ml4" extension with "mlg"
-- replace GEXTEND with GRAMMAR EXTEND
-- wrap every occurrence of OCaml code into braces { }
+In an effort to reduce dependency on camlp5, the use of several grammar macros
+is discouraged. Coq is now shipped with its own preprocessor, called coqpp,
+which serves the same purpose as camlp5.
+
+To perform the transition to coqpp macros, one first needs to change the
+extension of a macro file from `.ml4` to `.mlg`. Not all camlp5 macros are
+handled yet.
+
+Due to parsing constraints, the syntax of the macros is slightly different, but
+updating the source code is mostly a matter of straightforward
+search-and-replace. The main differences are summarized below.
+
+#### OCaml code
+
+Every piece of toplevel OCaml code needs to be wrapped into braces.
 
 For instance, code of the form
 ```
 let myval = 0
+```
+should be turned into
+```
+{
+let myval = 0
+}
+```
+
+#### TACTIC EXTEND
+
+Steps to perform:
+- replace the brackets enclosing OCaml code in actions with braces
+- if not there yet, add a leading `|̀  to the first rule
+
+For instance, code of the form:
+```
+TACTIC EXTEND my_tac
+  [ "tac1" int_or_var(i) tactic(t) ] -> [ mytac1 ist i t ]
+| [ "tac2" tactic(t) ] -> [ mytac2 t ]
+END
+```
+should be turned into
+```
+TACTIC EXTEND my_tac
+| [ "tac1" int_or_var(i) tactic(t) ] -> { mytac1 ist i t }
+| [ "tac2" tactic(t) ] -> { mytac2 t }
+END
+```
+
+#### VERNAC EXTEND
+
+Not handled yet.
+
+#### ARGUMENT EXTEND
+
+Not handled yet.
+
+#### GEXTEND
 
+Most plugin writers do not need this low-level interface, but for the sake of
+completeness we document it.
+
+Steps to perform are:
+- replace GEXTEND with GRAMMAR EXTEND
+- wrap every occurrence of OCaml code in actions into braces { }
+
+For instance, code of the form
+```
 GEXTEND Gram
    GLOBAL: my_entry;
 
@@ -119,10 +173,6 @@ END
 ```
 should be turned into
 ```
-{
-let myval = 0
-}
-
 GRAMMAR EXTEND Gram
    GLOBAL: my_entry;
 
@@ -133,9 +183,12 @@ my_entry:
 END
 ```
 
-Currently mlg files can only contain GRAMMAR EXTEND statements. They do not
-support TACTIC, VERNAC nor ARGUMENT EXTEND. In case you have a file containing
-both kinds at the same time, it is recommended splitting it in two.
+Caveats:
+- No `GLOBAL` entries mean that they are all local, while camlp5 special-cases
+  this as a shorthand for all global entries. Solution: always define a `GLOBAL`
+  section.
+- No complex patterns allowed in token naming. Solution: match on it inside the
+  OCaml quotation.
 
 ## Changes between Coq 8.7 and Coq 8.8
 
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index b35571e9c..48671c03b 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -10,9 +10,9 @@ versions of Proof General.
 
 A somewhat out-of-date description of the async state machine is
 [documented here](https://github.com/ejgallego/jscoq/blob/master/etc/notes/coq-notes.md).
-OCaml types for the protocol can be found in the [`ide/interface.mli` file](/ide/interface.mli).
+OCaml types for the protocol can be found in the [`ide/protocol/interface.ml` file](/ide/protocol/interface.ml).
 
-Changes to the XML protocol are documented as part of [`dev/doc/changes.txt`](/dev/doc/changes.txt).
+Changes to the XML protocol are documented as part of [`dev/doc/changes.md`](/dev/doc/changes.md).
 
 * [Commands](#commands)
   - [About](#command-about)