From 8c0f0b5250eef7130522b08263eff455d413ad64 Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Mon, 2 Oct 2023 06:38:54 -0400
Subject: [PATCH] docs: update RELEASES.md for #2502 (#2606)

---
 RELEASES.md | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/RELEASES.md b/RELEASES.md
index 04401f41ab..b826d02cd6 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -14,6 +14,9 @@ v4.2.0
 ---------
 
 * Improvements to Lake startup time ([#2572](https://github.com/leanprover/lean4/pull/2572), [#2573](https://github.com/leanprover/lean4/pull/2573))
+* `refine e` now replaces the main goal with metavariables which were created during elaboration of `e` and no longer captures pre-existing metavariables that occur in `e` ([#2502](https://github.com/leanprover/lean4/pull/2502)).
+  * This is accomplished via changes to `withCollectingNewGoalsFrom`, which also affects `elabTermWithHoles`, `refine'`, `calc` (tactic), and `specialize`. Likewise, all of these now only include newly-created metavariables in their output.
+  * Previously, both newly-created and pre-existing metavariables occurring in `e` were returned inconsistently in different edge cases, causing duplicated goals in the infoview (issue [#2495](https://github.com/leanprover/lean4/issues/2495)), erroneously closed goals (issue [#2434](https://github.com/leanprover/lean4/issues/2434)), and unintuitive behavior due to `refine e` capturing previously-created goals appearing unexpectedly in `e` (no issue; see PR).
 
 v4.1.0
 ---------