7 files changed, 72 insertions, 32 deletions
diff --git a/dev/doc/api.txt b/dev/doc/api.txt
deleted file mode 100644
index 5827257b53..0000000000
--- a/dev/doc/api.txt
+++ /dev/null
@@ -1,10 +0,0 @@
-Recommendations in using the API:
-
-The type of terms: constr (see kernel/constr.ml and kernel/term.ml)
-
-- On type constr, the canonical equality on CIC (up to
-  alpha-conversion and cast removal) is Constr.equal
-- The type constr is abstract, use mkRel, mkSort, etc. to build
-  elements in constr; use "kind_of_term" to analyze the head of a
-  constr; use destRel, destSort, etc. when the head constructor is
-  known
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index fefcb0937a..f3fc13e969 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -74,25 +74,25 @@ The Makefile is separated in several files :
 - Makefile.doc : specific rules for compiling the documentation.
 
 
-FIND_VCS_CLAUSE
+FIND_SKIP_DIRS
 ---------------
 
-The recommended style of using FIND_VCS_CLAUSE is for example
+The recommended style of using FIND_SKIP_DIRS is for example
 
- find . $(FIND_VCS_CLAUSE) '(' -name '*.example' ')' -print
- find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -or -name '*.foo' ')' -print
+ find . $(FIND_SKIP_DIRS) '(' -name '*.example' ')' -print
+ find . $(FIND_SKIP_DIRS) '(' -name '*.example' -or -name '*.foo' ')' -print
 
 1)
 The parentheses even in the one-criteria case is so that if one adds
 other conditions, e.g. change the first example to the second
 
- find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print
+ find . $(FIND_SKIP_DIRS) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print
 
 one is not tempted to write
 
- find . $(FIND_VCS_CLAUSE) -name '*.example' -and -not -name '*.bak.example' -print
+ find . $(FIND_SKIP_DIRS) -name '*.example' -and -not -name '*.bak.example' -print
 
-because this will not necessarily work as expected; $(FIND_VCS_CLAUSE)
+because this will not necessarily work as expected; $(FIND_SKIP_DIRS)
 ends with an -or, and how it combines with what comes later depends on
 operator precedence and all that. Much safer to override it with
 parentheses.
@@ -105,13 +105,13 @@ As to the -print at the end, yes it is necessary. Here's why.
 You are used to write:
  find . -name '*.example'
 and it works fine. But the following will not:
- find . $(FIND_VCS_CLAUSE) -name '*.example'
-it will also list things directly matched by FIND_VCS_CLAUSE
+ find . $(FIND_SKIP_DIRS) -name '*.example'
+it will also list things directly matched by FIND_SKIP_DIRS
 (directories we want to prune, in which we don't want to find
 anything). C'est subtil... Il y a effectivement un -print implicite à
 la fin, qui fait que la commande habituelle sans print fonctionne
 bien, mais dès que l'on introduit d'autres commandes dans le lot (le
--prune de FIND_VCS_CLAUSE), ça se corse à cause d'histoires de
+-prune de FIND_SKIP_DIRS), ça se corse à cause d'histoires de
 parenthèses du -print implicite par rapport au parenthésage dans la
 forme recommandée d'utilisation:
 
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 0728608f31..0f1a28028c 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,4 +1,28 @@
 =========================================
+= CHANGES BETWEEN COQ V8.7 AND COQ V8.8 =
+=========================================
+
+* ML API *
+
+We removed the following functions:
+
+- Universes.unsafe_constr_of_global: use Global.constr_of_global_in_context
+  instead. The returned term contains De Bruijn universe variables. If you don't
+  depend on universes being instantiated, simply drop the context.
+- Universes.unsafe_type_of_global: same as above with
+  Global.type_of_global_in_context
+
+We changed the type of the following functions:
+
+- Global.body_of_constant_body: now also returns the abstract universe context.
+  The returned term contains De Bruijn universe variables.
+- Global.body_of_constant: same as above.
+
+We renamed the following datatypes:
+
+  Pp.std_ppcmds -> Pp.t
+
+=========================================
 = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 =
 =========================================
 
@@ -8,6 +32,16 @@ Coq is compiled with -safe-string enabled and requires plugins to do
 the same. This means that code using `String` in an imperative way
 will fail to compile now. They should switch to `Bytes.t`
 
+* Plugin API *
+
+Coq 8.7 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 *
 
 Added two functions for declaring hooks to be executed in reduction
@@ -154,6 +188,9 @@ In Coqlib / reference location:
 - The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase
   was very specific. Use tclPROGRESS instead.
 
+- New (internal) tactical `tclINDEPENDENTL` that combined with enter_one allows
+  to iterate a non-unit tactic on all goals and access their returned values.
+
 - The unsafe flag of the Refine.refine function and its variants has been
   renamed and dualized into typecheck and has been made mandatory.
 
@@ -288,6 +325,10 @@ document type". This allows for a more uniform handling of printing
 
 - The legacy `Interp` call has been turned into a noop.
 
+- The `query` call has been modified, now it carries a mandatory
+  "route_id" integer parameter, that associated the result of such
+  query with its generated feedback.
+
 =========================================
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.md
index 79cde48849..7e9373b294 100644
--- a/dev/doc/debugging.txt
+++ b/dev/doc/debugging.md
@@ -1,7 +1,7 @@
 Debugging from Coq toplevel using Caml trace mechanism
 ======================================================
 
-  1. Launch bytecode version of Coq (coqtop.byte or coqtop -byte)
+  1. Launch bytecode version of Coq (coqtop.byte)
   2. Access Ocaml toplevel using vernacular command 'Drop.'
   3. Install load paths and pretty printers for terms, idents, ... using
      Ocaml command '#use "base_include";;' (use '#use "include";;' for 
@@ -25,8 +25,9 @@ Debugging from Coq toplevel using Caml trace mechanism
 Debugging from Caml debugger
 ============================
 
-   Needs tuareg mode in Emacs
-   Coq must be configured with -debug and -local (./configure -debug -local)
+   Requires [Tuareg mode](https://github.com/ocaml/tuareg) in Emacs.\
+   Coq must be configured with `-local` (`./configure -local`) and the
+   byte-code version of `coqtop` must have been generated with `make byte`.
 
    1. M-x camldebug
    2. give the binary name bin/coqtop.byte
@@ -53,6 +54,9 @@ Debugging from Caml debugger
      of each of error* functions or anomaly* functions in lib/util.ml
    - If "source db" fails, do a "make printers" and try again (it should build
      top_printers.cmo and the core cma files).
+   - If you have the OCAMLRUNPARAM environment variable set, Coq may hang on
+     startup when run from the debugger. If this happens, unset the variable,
+     re-start Emacs, and run the debugger again.
 
 Global gprof-based profiling
 ============================
@@ -65,14 +69,14 @@ Global gprof-based profiling
 Per function profiling
 ======================
 
-   1. To profile function foo in file bar.ml, add the following lines, just
-      after the definition of the function:
+   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;;
 
-     where foo is assumed to have three arguments (adapt using
-     Profile.profile1, Profile. profile2, etc).
+   where foo is assumed to have three arguments (adapt using
+   Profile.profile1, Profile. profile2, etc).
 
-     This has the effect to cumulate the time passed in foo under a
-     line of name "foo" which is displayed at the time coqtop exits.
+   This has the effect to cumulate the time passed in foo under a
+   line of name "foo" which is displayed at the time coqtop exits.
diff --git a/dev/doc/naming-conventions.tex b/dev/doc/naming-conventions.tex
index 349164948d..337b9226df 100644
--- a/dev/doc/naming-conventions.tex
+++ b/dev/doc/naming-conventions.tex
@@ -267,7 +267,7 @@ If the conclusion is in the other way than listed below, add suffix
 {forall x y:D, op (op' x y) = op' x (op y)}
 
 \itemrule{Idempotency of binary operator {\op} on domain {\D}}{Dop\_idempotent}
-{forall x:D, op x n = x}
+{forall x:D, op x x = x}
 
 \itemrule{Idempotency of unary operator {\op} on domain {\D}}{Dop\_idempotent}
 {forall x:D, op (op x) = op x}
diff --git a/dev/doc/notes-on-conversion b/dev/doc/notes-on-conversion.v
index a81f170c63..a81f170c63 100644
--- a/dev/doc/notes-on-conversion
+++ b/dev/doc/notes-on-conversion.v
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index 2ff82c6888..127b4a6d2d 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -308,15 +308,20 @@ CoqIDE typically sets `force` to `false`.
 
 -------------------------------
 
+### <a name="command-query">**Query(route_id: integer, query: string, stateId: integer)**</a>
+
+`routeId` can be used to distinguish the result of a particular query,
+`stateId` should be set to the state the query should be run.
 
-### <a name="command-query">**Query(query: string, stateId: integer)**</a>
-In practice, `stateId` is 0, but the effect is to perform the query on the currently-focused state.
 ```html
 <call val="Query">
   <pair>
+    <route_id val="${routeId}"/>
+  <pair>
     <string>${query}</string>
     <state_id val="${stateId}"/>
   </pair>
+  </pair>
 </call>
 ```
 #### *Returns*