aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES5
1 files changed, 5 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 96f02bc27c..70ed1bef01 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,6 +5,11 @@ 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
===================================