[ssr] implement {}/v as a short hand for {v}/v when v is an id

1 files changed, 6 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 40626bf06..6ad2cc548 100644
--- a/CHANGES
+++ b/CHANGES
@@ -75,6 +75,12 @@ SSReflect
   In particular rule 3 lets one write {x}/v even if v uses the variable x:
   indeed the view is executed before the renaming.
 
+- An empty clear switch is now accepted in intro patterns before a 
+  view application whenever the view is a variable.
+  One can now write {}/v to mean {v}/v.  Remark that {}/x is very similar
+  to the idiom {}e for the rewrite tactic (the equation e is used for
+  rewriting and then discarded).
+
 Changes from 8.8.0 to 8.8.1
 ===========================