Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.

Marking it as experimental.

1 files changed, 3 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 70ed1bef01..389572014e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -9,6 +9,9 @@ Tactics
 
 - Syntax "destruct !hyp" changed to "destruct (hyp)", and similarly
   for induction.
+- Syntax "p/c" for on-the-fly application of a lemma c before
+  introducing along pattern p changed to p%c1..%cn. The feature and
+  syntax are in experimental stage.
 
 Changes from V8.5beta2 to V8.5beta3
 ===================================