aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2015-12-05 00:42:24 +0100
committerHugo Herbelin2015-12-05 00:58:19 +0100
commitcbceffe424a6b4477eb822f3887776b587503cbd (patch)
tree03b784f5426564c7d74c54d4c7b83a3d6988b2ad
parent9ee4a02e9234ad6cebb3365881250d7539d00d03 (diff)
Fix CHANGES.
-rw-r--r--CHANGES11
1 files changed, 7 insertions, 4 deletions
diff --git a/CHANGES b/CHANGES
index 662b7b9a24..96f02bc27c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,10 @@
+Changes from V8.5beta3
+======================
+
+Specification language
+
+- Syntax "$(tactic)$" changed to "ltac:(tactic)".
+
Changes from V8.5beta2 to V8.5beta3
===================================
@@ -10,10 +17,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