From b8084d54e32caeb64670a9e42edaf7b01f072ce6 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 30 Aug 2023 14:44:23 +1000
Subject: [PATCH] doc: update RELEASES.md for rename of `getConst?` (#2482)

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

diff --git a/RELEASES.md b/RELEASES.md
index 8c04606dd5..6371f9bd98 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -10,6 +10,11 @@ Please check the [releases](https://github.com/leanprover/lean4/releases) page f
 v4.0.0
 ---------
 
+* [`Lean.Meta.getConst?` has been renamed](https://github.com/leanprover/lean4/pull/2454).
+  We have renamed `getConst?` to `getUnfoldableConst?` (and `getConstNoEx?` to `getUnfoldableConstNoEx?`).
+  These were not intended to be part of the public API, but downstream projects had been using them
+  (sometimes expecting different behaviour) incorrectly instead of `Lean.getConstInfo`.
+
 * [`dsimp` / `simp` / `simp_all` now fail by default if they make no progress](https://github.com/leanprover/lean4/pull/2336).
 
   This can be overriden with the `(config := { failIfUnchanged := false })` option.