From a9dc951e9068b18ee1cf0e51b2c4ae7a7c40354a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 15 May 2018 13:39:08 +0200 Subject: [ssr] implement {}/v as a short hand for {v}/v when v is an id --- CHANGES | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'CHANGES') 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 =========================== -- cgit v1.2.3