max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: update RELEASES.md for #3460 and #3482 (#3527)

Browse source
This commit is contained in:
Marc Huisinga 2024-02-29 11:42:54 +01:00 • committed by GitHub
parent b9f9ce874d
commit 970b6e59b1
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
RELEASES.md
View file

@ -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