Improving elimination with indices, getting rid of intrusive residual

local definitions...

1 files changed, 1 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index e0d65a635d..767ecf2e11 100644
--- a/CHANGES
+++ b/CHANGES
@@ -216,6 +216,7 @@ Tactics
     matching the given pattern is used
   - non-dependent destruct/induction on an hypothesis with premisses in
     an inductive type with indices is fixed
+  - residual local definitions are now correctly removed.
 
 Program