5 files changed, 47 insertions, 16 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index c69be4f4de..e616bd5663 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -12,16 +12,6 @@ All the bugs with a number below 1154 had to be renumbered, you can find
 a correspondence table [here](/dev/bugzilla2github_stripped.csv).
 All the other bugs kept their number.
 
-### Plugin API
-
-Coq 8.8 offers a new module overlay containing a proposed plugin API
-in `API/API.ml`; this overlay is enabled by adding the `-open API`
-flag to the OCaml compiler; this happens automatically for
-developments in the `plugin` folder and `coq_makefile`.
-
-However, `coq_makefile` can be instructed not to enable this flag by
-passing `-bypass-API`.
-
 ### ML API
 
 General deprecation
@@ -46,6 +36,11 @@ We changed the type of the following functions:
 
 - `Global.body_of_constant`: same as above.
 
+- `Constrinterp.*` generally, many functions that used to take an
+  `evar_map ref` have been now switched to functions that will work in
+  a functional way. The old style of passing `evar_map`s as references
+  is not supported anymore.
+
 We have changed the representation of the following types:
 
 - `Lib.object_prefix` is now a record instead of a nested tuple.
@@ -63,6 +58,13 @@ Declaration of printers for arguments used only in vernac command
   happen. An alternative is to register the corresponding argument as
   a value, using "Geninterp.register_val0 wit None".
 
+### XML IDE Protocol
+
+- Before 8.8, `Query` only executed the first command present in the
+ `query` string; starting with 8.8, the caller may include several
+ statements. This is useful for instance for temporarily setting an
+ option and then executing a command.
+
 ## Changes between Coq 8.6 and Coq 8.7
 
 ### Ocaml
diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md
index 7d3d811cc3..fd3cbd1bc3 100644
--- a/dev/doc/debugging.md
+++ b/dev/doc/debugging.md
@@ -22,8 +22,8 @@ Debugging from Coq toplevel using Caml trace mechanism
   printers too.
 
 
-Debugging from Caml debugger
-============================
+Debugging with ocamldebug from Emacs
+====================================
 
    Requires [Tuareg mode](https://github.com/ocaml/tuareg) in Emacs.\
    Coq must be configured with `-local` (`./configure -local`) and the
@@ -59,6 +59,29 @@ Debugging from Caml debugger
      from the debugger. If this happens, unset the variable, re-start Emacs, and 
      run the debugger again.
 
+Debugging with ocamldebug from the command line
+===============================================
+
+In the `coq` directory:
+1. (on Cygwin/Windows) Pass the `-no-custom` option to the `configure` script before building Coq.
+2. Run `make` (to compile the .v files)
+3. Run `make byte`
+4. (on Cygwin/Windows) Add the full pathname of the directory `.../kernel/byterun` to your bash PATH.
+   Alternatively, copy the file `kernel/byterun/dllcoqrun.dll` to a directory that is in the PATH.  (The
+   CAML_LD_LIBRARY_PATH mechanism described at the end of INSTALL isn't working.)
+5. Run `dev/ocamldebug-coq bin/coqtop.byte`  (on Cygwin/Windows, use `... bin/coqtop.byte.exe`)
+6. Enter `source db` to load printers
+7. Enter `set arguments -coqlib .` so Coq can find plugins, theories, etc.
+8. See the ocamldebug manual for more information.  A few points:
+   - use `break @ Printer 501` to set a breakpoint on line 501 in the Printer module (printer.ml).
+     `break` can be abbreviated as `b`.
+   - `backtrace` or `bt` to see the call stack
+   - `step` or `s` goes into called functions; `next` or `n` skips over them
+   - `list` or `li` shows the code just before and after the current stack frame
+   - `print <var>` or `p <var>` to see the value of a variable
+Note that `make byte` doesn't recompile .v files.  `make` recompiles all of them if there
+are changes in any .ml file--safer but much slower.
+
 Global gprof-based profiling
 ============================
 
@@ -73,8 +96,8 @@ Per function profiling
    To profile function foo in file bar.ml, add the following lines, just
    after the definition of the function:
 
-     let fookey = Profile.declare_profile "foo";;
-     let foo a b c = Profile.profile3 fookey foo a b c;;
+     let fookey = CProfile.declare_profile "foo";;
+     let foo a b c = CProfile.profile3 fookey foo a b c;;
 
    where foo is assumed to have three arguments (adapt using
    Profile.profile1, Profile. profile2, etc).
diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt
index 0c6d3ee80d..26f3d0ddc7 100644
--- a/dev/doc/setup.txt
+++ b/dev/doc/setup.txt
@@ -279,7 +279,7 @@ You can load them by switching to the window holding the "ocamldebug" shell and
 Some of the functions were you might want to set a breakpoint and see what happens next
 ---------------------------------------------------------------------------------------
 
-- Coqtop.start : This function is called by the code produced by "coqmktop".
+- Coqtop.start : This function is the main entry point of coqtop.
 - Coqtop.parse_args : This function is responsible for parsing command-line arguments.
 - Coqloop.loop : This function implements the read-eval-print loop.
 - Vernacentries.interp : This function is called to execute the Vernacular command user have typed.\
diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt
index 6a69c57934..ca3d520c70 100644
--- a/dev/doc/univpoly.txt
+++ b/dev/doc/univpoly.txt
@@ -12,7 +12,7 @@ type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
 
 type constr = ...
-  | Const of puniversess
+  | Const of puniverses
   | Ind of pinductive
   | Constr of pconstructor
   | Proj of constant * constr
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index 18f6288f6f..b35571e9ca 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -330,6 +330,12 @@ the STM API, `force` triggers a `Join`.
   <string>${message}</string>
 </value>
 ```
+
+Before 8.8, `Query` only executed the first command present in the
+`query` string; starting with 8.8, the caller may include several
+statements. This is useful for instance for temporarily setting an
+option and then executing a command.
+
 -------------------------------