1 files changed, 113 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 0581a5f850..4135ddd2db 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,73 @@
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
 
+** Notation_ops **
+
+Use Glob_ops.glob_constr_eq instead of Notation_ops.eq_glob_constr.
+
+** Logging and Pretty Printing: **
+
+* Printing functions have been removed from `Pp.mli`, which is now a
+  purely pretty-printing interface. Functions affected are:
+
+```` ocaml
+val pp          : std_ppcmds -> unit
+val ppnl        : std_ppcmds -> unit
+val pperr       : std_ppcmds -> unit
+val pperrnl     : std_ppcmds -> unit
+val pperr_flush : unit -> unit
+val pp_flush    : unit -> unit
+val flush_all   : unit -> unit
+val msg         : std_ppcmds -> unit
+val msgnl       : std_ppcmds -> unit
+val msgerr      : std_ppcmds -> unit
+val msgerrnl    : std_ppcmds -> unit
+val message     : string -> unit
+````
+
+  which are no more available. Users of `Pp.pp msg` should now use the
+  proper `Feedback.msg_*` function. Clients also have no control over
+  flushing, the back end takes care of it.
+
+* Feedback related functions and definitions have been moved to the
+  `Feedback` module. `message_level` has been renamed to
+  level. Functions moved from Pp to Feedback are:
+
+```` ocaml
+val set_logger      : logger -> unit
+val std_logger      : logger
+val emacs_logger    : logger
+val feedback_logger : logger
+````
+
+* We now provide several loggers, `log_via_feedback` is removed in
+  favor of `set_logger feedback_logger`. Output functions are:
+
+```` ocaml
+val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+val msg_info    : Pp.std_ppcmds -> unit
+val msg_notice  : Pp.std_ppcmds -> unit
+val msg_warning : Pp.std_ppcmds -> unit
+val msg_error   : Pp.std_ppcmds -> unit
+val msg_debug   : Pp.std_ppcmds -> unit
+````
+
+  with the `msg_*` functions being just an alias for `logger $Level`.
+
+* The main feedback functions are:
+
+```` ocaml
+val set_feeder : (feedback -> unit) -> unit
+val feedback : ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit
+val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit
+````
+  Note that `feedback` doesn't take two parameters anymore. After
+  refactoring the following function has been removed:
+
+```` ocaml
+val get_id_for_feedback : unit -> edit_or_state_id * route_id
+````
+
 - The interface of the Context module was changed.
   Related types and functions were put in separate submodules.
   The mapping from old identifiers to new identifiers is the following:
@@ -66,6 +133,52 @@
     Context.Named.t = LocalAssum of Names.Id.t * Constr.t
 	            | LocalDef of Names.Id.t * Constr.t * Constr.t
 
+- The various EXTEND macros do not handle specially the Coq-defined entries
+  anymore. Instead, they just output a name that have to exist in the scope
+  of the ML code. The parsing rules (VERNAC) ARGUMENT EXTEND will look for
+  variables "$name" of type Gram.entry, while the parsing rules of
+  (VERNAC COMMAND | TACTIC) EXTEND, as well as the various TYPED AS clauses will
+  look for variables "wit_$name" of type Genarg.genarg_type. The small DSL
+  for constructing compound entries still works over this scheme. Note that in
+  the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound
+  in the parsing rules, so beware of recursive calls.
+
+- Evarutil was split in two parts. The new Evardefine file exposes functions
+define_evar_* mostly used internally in the unification engine.
+
+- The Refine module was move out of Proofview.
+
+    Proofview.Refine.* --->  Refine.*
+
+- A statically monotonous evarmap type was introduced in Sigma. Not all the API
+  has been converted, so that the user may want to use compatibility functions
+  Sigma.to_evar_map and Sigma.Unsafe.of_evar_map or Sigma.Unsafe.of_pair when
+  needed. Code can be straightforwardly adapted in the following way:
+
+  let (sigma, x1) = ... in
+  ...
+  let (sigma, xn) = ... in
+  (sigma, ans)
+
+  should be turned into:
+
+  open Sigma.Notations
+
+  let Sigma (x1, sigma, p1) = ... in
+  ...
+  let Sigma (xn, sigma, pn) = ... in
+  Sigma (ans, sigma, p1 +> ... +> pn)
+
+- The Proofview.Goal.*enter family of functions now takes a polymorphic
+  continuation given as a record as an argument.
+
+  Proofview.Goal.enter begin fun gl -> ... end
+
+  should be turned into
+
+  open Proofview.Notations
+
+  Proofview.Goal.enter { enter = begin fun gl -> ... end }
 
 =========================================
 = CHANGES BETWEEN COQ V8.4 AND COQ V8.5 =