1 files changed, 217 insertions, 10 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index ab78b095..ca73cd63 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,3 +1,205 @@
+## Changes between Coq 8.8 and Coq 8.9
+
+### ML API
+
+Names
+
+- In `Libnames`, the type `reference` and its two constructors `Qualid` and
+  `Ident` have been removed in favor of `qualid`. `Qualid` is now the identity,
+  `Ident` can be replaced by `qualid_of_ident`. Matching over `reference` can be
+  replaced by a test using `qualid_is_ident`. Extracting the `ident` part of a
+  `qualid` can be done using `qualid_basename`.
+
+Misctypes
+
+- Syntax for universe sorts and kinds has been moved from `Misctypes`
+  to `Glob_term`, as these are turned into kernel terms by
+  `Pretyping`.
+
+Proof engine
+
+- More functions have been changed to use `EConstr`, notably the
+  functions in `Evd`, and in particular `Evd.define`.
+
+  Note that the core function `EConstr.to_constr` now _enforces_ by
+  default that the resulting term is ground, that is to say, free of
+  Evars. This is usually what you want, as open terms should be of
+  type `EConstr.t` to benefit from the invariants the `EConstr` API is
+  meant to guarantee.
+
+  In case you'd like to violate this API invariant, you can use the
+  `abort_on_undefined_evars` flag to `EConstr.to_constr`, but note
+  that setting this flag to false is deprecated so it is only meant to
+  be used as to help port pre-EConstr code.
+
+- A few type alias have been deprecated, in all cases the message
+  should indicate what the canonical form is. An important change is
+  the move of `Globnames.global_reference` to `Names.GlobRef.t`.
+
+- Unification API returns `evar_map option` instead of `bool * evar_map`
+  with the guarantee that the `evar_map` was unchanged if the boolean
+  was false.
+
+ML Libraries used by Coq
+
+- Introduction of a `Smart` module for collecting `smart*` functions, e.g.
+  `Array.Smart.map`.
+- Uniformization of some names, e.g. `Array.Smart.fold_left_map` instead
+  of `Array.smartfoldmap`.
+
+Printer.ml API
+
+- The mechanism in `Printer` that allowed dynamically overriding `pr_subgoals`,
+  `pr_subgoal` and `pr_goal` was removed to simplify the code.  It was
+  earlier used by PCoq.
+
+Kernel
+
+- The following renamings happened:
+  - `Context.Rel.t` into `Constr.rel_context`
+  - `Context.Named.t` into `Constr.named_context`
+  - `Context.Compacted.t` into `Constr.compacted_context`
+  - `Context.Rel.Declaration.t` into `Constr.rel_declaration`
+  - `Context.Named.Declaration.t` into `Constr.named_declaration`
+  - `Context.Compacted.Declaration.t` into `Constr.compacted_declaration`
+
+Source code organization
+
+- We have eliminated / fused some redundant modules and relocated a
+  few interfaces files. The `intf` folder is gone, and now for example
+  `Constrexpr` is located in `interp/`, `Vernacexpr` in `vernac/` and
+  so on. Changes should be compatible, but in a few cases stricter
+  layering requirements may mean that functions have moved. In all
+  cases adapting is a matter of changing the module name.
+
+Vernacular commands
+
+- The implementation of vernacular commands has been refactored so it
+  is self-contained now, including the parsing and extension
+  mechanisms. This involves a couple of non-backward compatible
+  changes due to layering issues, where some functions have been moved
+  from `Pcoq` to `Pvernac` and from `Vernacexpr` to modules in
+  `tactics/`. In all cases adapting is a matter of changing the module
+  name.
+
+Primitive number parsers
+
+- For better modularity, the primitive parsers for `positive`, `N` and `Z`
+  have been split over three files (`plugins/syntax/positive_syntax.ml`,
+  `plugins/syntax/n_syntax.ml`, `plugins/syntax/z_syntax.ml`).
+
+Parsing
+
+- Manual uses of the `Pcoq.Gram` module have been deprecated. Wrapper modules
+  `Pcoq.Entry` and `Pcoq.Parsable` were introduced to replace it.
+
+Termops
+
+- Internal printing functions have been placed under the
+  `Termops.Internal` namespace.
+
+### Unit testing
+
+The test suite now allows writing unit tests against OCaml code in the Coq
+code base. Those unit tests create a dependency on the OUnit test framework.
+
+### Transitioning away from Camlp5
+
+In an effort to reduce dependency on camlp5, the use of several grammar macros
+is discouraged. Coq is now shipped with its own preprocessor, called coqpp,
+which serves the same purpose as camlp5.
+
+To perform the transition to coqpp macros, one first needs to change the
+extension of a macro file from `.ml4` to `.mlg`. Not all camlp5 macros are
+handled yet.
+
+Due to parsing constraints, the syntax of the macros is slightly different, but
+updating the source code is mostly a matter of straightforward
+search-and-replace. The main differences are summarized below.
+
+#### OCaml code
+
+Every piece of toplevel OCaml code needs to be wrapped into braces.
+
+For instance, code of the form
+```
+let myval = 0
+```
+should be turned into
+```
+{
+let myval = 0
+}
+```
+
+#### TACTIC EXTEND
+
+Steps to perform:
+- replace the brackets enclosing OCaml code in actions with braces
+- if not there yet, add a leading `|` to the first rule
+
+For instance, code of the form:
+```
+TACTIC EXTEND my_tac
+  [ "tac1" int_or_var(i) tactic(t) ] -> [ mytac1 ist i t ]
+| [ "tac2" tactic(t) ] -> [ mytac2 t ]
+END
+```
+should be turned into
+```
+TACTIC EXTEND my_tac
+| [ "tac1" int_or_var(i) tactic(t) ] -> { mytac1 ist i t }
+| [ "tac2" tactic(t) ] -> { mytac2 t }
+END
+```
+
+#### VERNAC EXTEND
+
+Not handled yet.
+
+#### ARGUMENT EXTEND
+
+Not handled yet.
+
+#### GEXTEND
+
+Most plugin writers do not need this low-level interface, but for the sake of
+completeness we document it.
+
+Steps to perform are:
+- replace `GEXTEND` with `GRAMMAR EXTEND`
+- wrap every occurrence of OCaml code in actions into braces `{ }`
+
+For instance, code of the form
+```
+GEXTEND Gram
+   GLOBAL: my_entry;
+
+my_entry:
+[ [ x = bar; y = qux -> do_something x y
+  | "("; z = LIST0 my_entry; ")" -> do_other_thing z
+] ];
+END
+```
+should be turned into
+```
+GRAMMAR EXTEND Gram
+   GLOBAL: my_entry;
+
+my_entry:
+[ [ x = bar; y = qux -> { do_something x y }
+  | "("; z = LIST0 my_entry; ")" -> { do_other_thing z }
+] ];
+END
+```
+
+Caveats:
+- No `GLOBAL` entries mean that they are all local, while camlp5 special-cases
+  this as a shorthand for all global entries. Solution: always define a `GLOBAL`
+  section.
+- No complex patterns allowed in token naming. Solution: match on it inside the
+  OCaml quotation.
+
 ## Changes between Coq 8.7 and Coq 8.8
 
 ### Bug tracker
@@ -16,7 +218,7 @@ All the other bugs kept their number.
 
 General deprecation
 
-- All functions marked [@@ocaml.deprecated] in 8.7 have been
+- All functions marked `[@@ocaml.deprecated]` in 8.7 have been
   removed. Please, make sure your plugin is warning-free in 8.7 before
   trying to port it over 8.8.
 
@@ -44,8 +246,8 @@ 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
+- `Constrinterp.*`: generally, many functions that used to take an
+  `evar_map ref` have now been switched to functions that will work in
   a functional way. The old style of passing `evar_map`s as references
   is not supported anymore.
 
@@ -63,16 +265,21 @@ We have changed the representation of the following types:
 
 Some tactics and related functions now support static configurability, e.g.:
 
-- injectable, dEq, etc. takes an argument ~keep_proofs which,
-  - if None, tells to behave as told with the flag Keep Proof Equalities
-  - if Some b, tells to keep proof equalities iff b is true
+- `injectable`, `dEq`, etc. take an argument `~keep_proofs` which,
+  - if `None`, tells to behave as told with the flag `Keep Proof Equalities`
+  - if `Some b`, tells to keep proof equalities iff `b` is true
 
 Declaration of printers for arguments used only in vernac command
 
-- It should now use "declare_extra_vernac_genarg_pprule" rather than
-  "declare_extra_genarg_pprule", otherwise, a failure at runtime might
+- It should now use `declare_extra_vernac_genarg_pprule` rather than
+  `declare_extra_genarg_pprule`, otherwise, a failure at runtime might
   happen. An alternative is to register the corresponding argument as
-  a value, using "Geninterp.register_val0 wit None".
+  a value, using `Geninterp.register_val0 wit None`.
+
+Types Alias deprecation and type relocation.
+
+- A few type alias have been deprecated, in all cases the message
+  should indicate what the canonical form is.
 
 ### STM API
 
@@ -110,7 +317,7 @@ functions when some given constants are traversed:
 
   * `declare_reduction_effect`: to declare a hook to be applied when some
   constant are visited during the execution of some reduction functions
-  (primarily cbv).
+  (primarily `cbv`).
 
   * `set_reduction_effect`: to declare a constant on which a given effect
   hook should be called.