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.