From c7fad1815ca1a9e00bc3435fa45d3ce4a4f2a964 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 30 Sep 2022 09:31:03 -0700 Subject: [PATCH] chore: update release notes --- RELEASES.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/RELEASES.md b/RELEASES.md index 51b904c2fe..d03983c5ef 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -1,6 +1,14 @@ Unreleased --------- +* [Hover information for `cases`/`induction` case names](https://github.com/leanprover/lean4/pull/1660). + +* [Prefer longer parse even if unsuccessful](https://github.com/leanprover/lean4/pull/1658). + +* [Show declaration module in hover](https://github.com/leanprover/lean4/pull/1638). + +* [New `conv` mode structuring tactics](https://github.com/leanprover/lean4/pull/1636). + * `simp` can track information and can print an equivalent `simp only`. [PR #1626](https://github.com/leanprover/lean4/pull/1626). * Enforce uniform indentation in tactic blocks / do blocks. See issue [#1606](https://github.com/leanprover/lean4/issues/1606).