1 files changed, 21 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 24c4cfec0..234d6c0db 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,27 @@ Tools
 - Coq_makefile lets one override or extend the following variables from
   the command line: COQFLAGS, COQCHKFLAGS, COQDOCFLAGS.
 
+Vernacular Commands
+
+- Removed deprecated commands Arguments Scope and Implicit Arguments
+  (not the option). Use the Arguments command instead.
+
+Tactic language
+
+- Support for fix/cofix added in Ltac "match" and "lazymatch".
+
+- Ltac backtraces now contain include trace information about tactics
+  called by OCaml-defined tactics.
+
+Changes from 8.8+beta1 to 8.8.0
+===============================
+
+Tools
+
+- Asynchronous proof delegation policy was fixed. Since version 8.7
+  Coq was ignoring previous runs and the -async-proofs-delegation-threshold
+  option did not have the expected behavior.
+
 Changes from 8.7.2 to 8.8+beta1
 ===============================