Update CHANGES and credits for 8.6beta1.

1 files changed, 6 insertions, 7 deletions

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 4f4f404422..f36969e821 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1094,13 +1094,11 @@ Hugo Herbelin, Matthieu Sozeau and the {\Coq} development team\\
 year of (now time-based) development, about 450 bugs were resolved and
 over 100 contributions integrated. The main user visible changes are:
 \begin{itemize}
-\item A new, state-of-the-art universe constraint checker that
-  can outperform the previous version by an order of magnitude, by
+\item A new, faster state-of-the-art universe constraint checker, by
   Jacques-Henri Jourdan.
 \item In CoqIDE and other asynchronous interfaces, more fine-grained
-  asynchronous processing and error reporting by Enrico Tassi. In
-  asynchronous mode {\Coq} is now capable of recovering from errors 
-  and continue processing the document.
+  asynchronous processing and error reporting by Enrico Tassi, making {\Coq}
+  capable of recovering from errors and continue processing the document.
 \item More access to the proof engine features from Ltac: goal
   management primitives, range selectors and a {\tt typeclasses
     eauto} engine handling multiple goals and multiple successes, by
@@ -1111,8 +1109,9 @@ over 100 contributions integrated. The main user visible changes are:
   into errors or ignore them selectively by Maxime Dénès, Guillaume
   Melquiond, Pierre-Marie Pédrot and others.
 \item Irrefutable patterns in abstractions, by Daniel de Rauglaudre.
-\item Integration of {\tt ssreflect}'s subterm selection algorithm by
-  Enrico Tassi.
+\item The {\tt ssreflect} subterm selection algorithm by Georges Gonthier and
+  Enrico Tassi is now accessible to tactic writers through the {\tt ssrmatching}
+  plugin.
 \item Integration of {\tt LtacProf}, a profiler for {\tt Ltac} by Jason
   Gross, Paul Steckler, Enrico Tassi and Tobias Tebbi.
 \end{itemize}