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(-)

(limited to 'CHANGES')

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


From 387351b4c0ffeff65d8a7192f5073cfd4bd20f53 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 5 Dec 2015 00:14:37 +0100
Subject: Changing "destruct !hyp" into "destruct (hyp)" (and similarly for
 induction) based on a suggestion of Guillaume M. (done like this in
 ssreflect).

This is actually consistent with the hack of using "destruct (1)" to
mean the term 1 by opposition to the use of "destruct 1" to mean the
first non-dependent hypothesis of the goal.
---
 CHANGES | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'CHANGES')

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
 ===================================
 
-- 
cgit v1.2.3