From 970b6e59b1851e33f469df6569a655b8ca62c5cf Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Thu, 29 Feb 2024 11:42:54 +0100 Subject: [PATCH] doc: update RELEASES.md for #3460 and #3482 (#3527) --- RELEASES.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/RELEASES.md b/RELEASES.md index 5c6054f6f0..4b11b6f175 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -83,6 +83,10 @@ v4.7.0 (development in progress) * Improved the error messages produced by the `decide` tactic. [#3422](https://github.com/leanprover/lean4/pull/3422) +* Improved auto-completion performance. [#3460](https://github.com/leanprover/lean4/pull/3460) + +* Changed call hierarchy to sort entries and strip private header from names displayed in the call hierarchy. [#3482](https://github.com/leanprover/lean4/pull/3482) + Breaking changes: * `Lean.withTraceNode` and variants got a stronger `MonadAlwaysExcept` assumption to fix trace trees not being built on elaboration runtime exceptions. Instances for most elaboration