Merge branch 'v8.5'

1 files changed, 12 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index 9da642b0f6..3eed3dca07 100644
--- a/CHANGES
+++ b/CHANGES
@@ -12,6 +12,18 @@ Program
 - The "Shrink Obligations" flag now applies to all obligations, not only those
   solved by the automatic tactic.
 
+Changes from V8.5beta3
+======================
+
+Specification language
+
+- Syntax "$(tactic)$" changed to "ltac:(tactic)".
+
+Tactics
+
+- Syntax "destruct !hyp" changed to "destruct (hyp)", and similarly
+  for induction.
+
 Changes from V8.5beta2 to V8.5beta3
 ===================================
 
@@ -24,10 +36,6 @@ Vernacular commands
   introducing it.
 - New command "Show id" to show goal named id.
 
-Specification language
-
-- Syntax "$(tactic)$" changed to "ltac: tactic".
-
 Tactics
 
 - New flag "Regular Subst Tactic" which fixes "subst" in situations where