From 43d6eb144e7a84af7c6eb40e60c9d2538367d6eb Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 1 Mar 2024 06:38:18 +0100 Subject: [PATCH] chore: add error recovery to RELEASES.md (#3540) Adds the missing RELEASES.md from #3413. Apologies for the oversight! --- RELEASES.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/RELEASES.md b/RELEASES.md index eb9ae5067b..804073b6dd 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -91,6 +91,8 @@ v4.7.0 (development in progress) * 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) +* There is now a low-level error recovery combinator in the parsing framework, primarily intended for DSLs. [#3413](https://github.com/leanprover/lean4/pull/3413) + 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