From cbceffe424a6b4477eb822f3887776b587503cbd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 5 Dec 2015 00:42:24 +0100 Subject: Fix CHANGES. --- CHANGES | 11 +++++++---- 1 file 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 -- cgit v1.2.3