[ssr] simplify delayed clears

- we always rename
- we compile {clear}/view to /view{clear}

1 files changed, 14 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index c36f59726b..40626bf066 100644
--- a/CHANGES
+++ b/CHANGES
@@ -61,6 +61,20 @@ Coq binaries and process model
   `coq{proof,tactic,query}worker` are in charge of task-specific and
   parallel proof checking.
 
+SSReflect
+
+- The implementation of delayed clear switches in intro patterns
+  is now simpler to explain:
+  1. The immediate effect of a clear switch like {x} is to rename the
+     variable x to _x_ (i.e. a reserved identifier that cannot be mentioned
+     explicitly)
+  2. The delayed effect of {x} is that _x_ is cleared at the end of the intro
+     pattern
+  3. A clear switch immediately before a view application like {x}/v is
+     translated to /v{x}.
+  In particular rule 3 lets one write {x}/v even if v uses the variable x:
+  indeed the view is executed before the renaming.
+
 Changes from 8.8.0 to 8.8.1
 ===========================