From 3e79ddda27c299a0e66fc996d52fa15fcf4421d8 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 15 Oct 2023 13:51:58 +1100 Subject: [PATCH] chore: add items to RELEASES.md (#2687) --- RELEASES.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/RELEASES.md b/RELEASES.md index f1e7fccccf..d9de53dbd5 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -11,10 +11,11 @@ v4.3.0 (development in progress) --------- * [isDefEq cache for terms not containing metavariables.](https://github.com/leanprover/lean4/pull/2644). - * [Cancel outstanding tasks on document edit in the language server](https://github.com/leanprover/lean4/pull/2648). - +* Make [`Environment.mk`](https://github.com/leanprover/lean4/pull/2604) and [`Environment.add`](https://github.com/leanprover/lean4/pull/2642) private, and add [`replay`](https://github.com/leanprover/lean4/pull/2617) as a safer alternative. * `IO.Process.output` no longer inherits the standard input of the caller. +* [Do not inhibit caching](https://github.com/leanprover/lean4/pull/2612) of default-level `match` reduction. +* [List the valid case tags](https://github.com/leanprover/lean4/pull/2629) when the user writes an invalid one. * The derive handler for `DecidableEq` [now handles](https://github.com/leanprover/lean4/pull/2591) mutual inductive types. * [Show path of failed import in Lake](https://github.com/leanprover/lean4/pull/2616). * [Fix linker warnings on macOS](https://github.com/leanprover/lean4/pull/2598).