2 files changed, 72 insertions, 2 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 3de938d774..8d2d055908 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,4 +1,74 @@
 =========================================
+= CHANGES BETWEEN COQ V8.6 AND COQ V8.7 =
+=========================================
+
+* ML API *
+
+We renamed the following functions:
+
+  Context.Rel.Declaration.fold   -> Context.Rel.Declaration.fold_constr
+  Context.Named.Declaration.fold -> Context.Named.Declaration.fold_constr
+  Printer.pr_var_list_decl       -> Printer.pr_compacted_decl
+  Printer.pr_var_decl            -> Printer.pr_named_decl
+  Nameops.lift_subscript         -> Nameops.increment_subscript
+
+We removed the following functions:
+
+  Termops.compact_named_context_reverse ... practical substitute is Termops.compact_named_context
+  Namegen.to_avoid                      ... equivalent substitute is Names.Id.List.mem
+
+We renamed the following modules:
+
+  Context.ListNamed -> Context.Compacted
+
+The following type aliases where removed
+
+  Context.section_context    ... it was just an alias for "Context.Named.t" which is still available
+
+The module Constrarg was merged into Stdarg.
+
+** Ltac API **
+
+Many Ltac specific API has been moved in its own ltac/ folder. Amongst other
+important things:
+
+- Pcoq.Tactic -> Pltac
+- Constrarg.wit_tactic -> Tacarg.wit_tactic
+- Constrarg.wit_ltac -> Tacarg.wit_ltac
+- API below ltac/ that accepted a *_tactic_expr now accept a *_generic_argument
+  instead
+- Some printing functions were moved from Pptactic to Pputils
+- A part of Tacexpr has been moved to Tactypes
+
+The folder itself has been turned into a plugin. This does not change much,
+but because it is a packed plugin, it may wreak havoc for third-party plugins
+depending on any module defined in the ltac/ directory. Namely, even if
+everything looks OK at compile time, a plugin can fail to load at link time
+because it mistakenly looks for a module Foo instead of Ltac_plugin.Foo, with
+an error of the form:
+
+Error: while loading myplugin.cmxs, no implementation available for Foo.
+
+In particular, most EXTEND macros will trigger this problem even if they
+seemingly do not use any Ltac module, as their expansion do.
+
+The solution is simple, and consists in adding a statement "open Ltac_plugin"
+in each file using a Ltac module, before such a module is actually called. An
+alternative solution would be to fully qualify Ltac modules, e.g. turning any
+call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not
+work for EXTEND macros though.
+
+** Error handling **
+
+- All error functions now take an optional parameter `?loc:Loc.t`. For
+  functions that used to carry a suffix `_loc`, such suffix has been
+  dropped.
+
+- `errorlabstrm` has been removed in favor of `user_err`.
+
+- The header parameter to `user_err` has been made optional.
+
+=========================================
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
 
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
index f0df2fc371..79cde48849 100644
--- a/dev/doc/debugging.txt
+++ b/dev/doc/debugging.txt
@@ -51,8 +51,8 @@ Debugging from Caml debugger
      failure/error/anomaly has been raised
    - Alternatively, for an error or an anomaly, add breakpoints in the middle  
      of each of error* functions or anomaly* functions in lib/util.ml
-   - If "source db" fails, recompile printers.cma with
-     "make dev/printers.cma" and try again
+   - If "source db" fails, do a "make printers" and try again (it should build
+     top_printers.cmo and the core cma files).
 
 Global gprof-based profiling
 ============================