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.

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
 ===================================