From f875c2d107c7a843bb1ca3f56b77e96b86bb680e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Apr 2022 10:32:36 -0700 Subject: [PATCH] chore: update release notes --- RELEASES.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/RELEASES.md b/RELEASES.md index 2ee8f4f85b..acd6414d7c 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -16,6 +16,8 @@ inductive LE' : Nat → Nat → Prop where In both cases, the inductive family has one parameter and one index. Recall that the actual number of parameters can be retrieved using the command `#print`. +* Remove support for `{}` annotation in the `structure` command. + * Several improvements to LSP server. Examples: "jump to definition" in mutually recursive sections, fixed incorrect hover information in "match"-expression patterns, "jump to definition" for pattern variables, fixed auto-completion in function headers, etc. * In `macro ... xs:p* ...` and similar macro bindings of combinators, `xs` now has the correct type `Array Syntax`