1 files changed, 91 insertions, 1 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 8ea1638c9..bcda4ff50 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -51,12 +51,96 @@ In Constrexpr_ops:
   interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second
   ones were preserving the original sharing of the type.
 
+In Nameops:
+
+  The API has been made more uniform. New combinators added in the
+  "Name" space name. Function "out_name" now fails with IsAnonymous
+  rather than with Failure "Nameops.out_name".
+
+Location handling and AST attributes:
+
+  Location handling has been reworked. First, Loc.ghost has been
+  removed in favor of an option type, all objects carrying an optional
+  source code location have been switched to use `Loc.t option`.
+
+  Storage of location information has been also refactored. The main
+  datatypes representing Coq AST (constrexpr, glob_expr) have been
+  switched to a generic "node with attributes" representation `'a
+  CAst.ast`, which is a record of the form:
+
+```ocaml
+type 'a ast = private {
+  v   : 'a;
+  loc : Loc.t option;
+  ...
+}
+```
+  consumers of AST nodes are recommended to use accessor-based pattern
+  matching `{ v; loc }` to destruct `ast` object. Creation is done
+  with `CAst.make ?loc obj`, where the attributes are optional. Some
+  convenient combinators are provided in the module. A typical match:
+```
+| CCase(loc, a1) -> CCase(loc, f a1)
+```
+  is now done as:
+```
+| { v = CCase(a1); loc } -> CAst.make ?loc @@ CCase(f a1)
+```
+  or even better, if plan to preserve the attributes you can wrap your
+  top-level function in `CAst.map` to have:
+
+```
+| CCase(a1) -> CCase(f a1)
+```
+
+  This scheme based on records enables easy extensibility of the AST
+  node type without breaking compatibility.
+
+  Not all objects carrying a location have been converted to the
+  generic node representation, some of them may be converted in the
+  future, for some others the abstraction is not just worth it.
+
+  Thus, we still maintain a `'a Loc.located == Loc.t option * a'`,
+  tuple type which should be treated as private datatype (ok to match
+  against, but forbidden to manually build), and it is mandatory to
+  use it for objects that carry a location. This policy has been
+  implemented in the whole code base. Matching a located object hasn't
+  changed, however, `Loc.tag ?loc obj` must be used to build one.
+
+In GOption:
+
+  Support for non-synchronous options has been removed. Now all
+  options are handled as a piece of normal document state, and thus
+  passed to workers, etc... As a consequence, the field
+  `Goptions.optsync` has been removed.
+
+In Coqlib / reference location:
+
+  We have removed from Coqlib functions returning `constr` from
+  names. Now it is only possible to obtain references, that must be
+  processed wrt the particular needs of the client.
+  We have changed in constrintern the functions returnin `constr` as
+  well to return global references instead.
+
+  Users of `coq_constant/gen_constant` can do
+  `Universes.constr_of_global (find_reference dir r)` _however_ note
+  the warnings in the `Universes.constr_of_global` in the
+  documentation. It is very likely that you were previously suffering
+  from problems with polymorphic universes due to using
+  `Coqlib.coq_constant` that used to do this. You must rather use
+  `pf_constr_of_global` in tactics and `Evarutil.new_global` variants
+  when constructing terms in ML (see univpoly.txt for more information).
+
 ** Tactic API **
 
 - pf_constr_of_global now returns a tactic instead of taking a continuation.
   Thus it only generates one instance of the global reference, and it is the
   caller's responsibility to perform a focus on the goal.
 
+- pf_global, construct_reference, global_reference,
+  global_reference_in_absolute_module now return a global_reference
+  instead of a constr.
+
 - The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase
   was very specific. Use tclPROGRESS instead.
 
@@ -93,13 +177,19 @@ 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.
 
+** Additional changes in tactic extensions **
+
+Entry "constr_with_bindings" has been renamed into
+"open_constr_with_bindings". New entry "constr_with_bindings" now
+uses type classes and rejects terms with unresolved holes.
+
 ** 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`.
+- `errorlabstrm` and `error` has been removed in favor of `user_err`.
 
 - The header parameter to `user_err` has been made optional.