3 files changed, 41 insertions, 11 deletions
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..57c7a97d58 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,4 +1,24 @@
 =========================================
+= 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.
+
+=========================================
 = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 =
 =========================================
 
@@ -8,6 +28,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
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}