From e470dad36c6beb03affe06a045292f2ec48f5e70 Mon Sep 17 00:00:00 2001 From: tydeu Date: Fri, 5 Aug 2022 23:30:46 -0400 Subject: [PATCH] chore: update Lake --- RELEASES.md | 4 ++-- src/lake | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/RELEASES.md b/RELEASES.md index 452c3b2f35..8fe4347579 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -1,6 +1,8 @@ Unreleased --------- +* Update Lake to v4.0.0. See the [v4.0.0 release notes](https://github.com/leanprover/lake/releases/tag/v4.0.0) for detailed changes. + * Mutual declarations in different namespaces are now supported. Example: ```lean mutual @@ -251,8 +253,6 @@ Unreleased end Nat ``` -* Update Lake to v3.2.1. See the [v3.2.1 release notes](https://github.com/leanprover/lake/releases/tag/v3.2.1) for detailed changes. - * Add support for `CommandElabM` monad at `#eval`. Example: ```lean import Lean diff --git a/src/lake b/src/lake index dcf8e1fc40..b899c0abac 160000 --- a/src/lake +++ b/src/lake @@ -1 +1 @@ -Subproject commit dcf8e1fc406acfd4dbbfd691f4ecf76966fae407 +Subproject commit b899c0abac7d6c7ad69c06cd5b7964ac5684d3f0