6 files changed, 49 insertions, 22 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 159be9a582..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.
 
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
index 79cde48849..3e2b435b3e 100644
--- a/dev/doc/debugging.txt
+++ b/dev/doc/debugging.txt
@@ -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 
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