From 40129203b2afb3906701afbe9dd67f1713b82151 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 17 Apr 2022 13:55:46 -0700
Subject: [PATCH] chore: update `RELEASES.md`

---
 RELEASES.md | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/RELEASES.md b/RELEASES.md
index acd6414d7c..0a45bdf63a 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -1,6 +1,25 @@
 Unreleased
 ---------
 
+* Add `save` tactic for creating checkpoints more conveniently. Example:
+```lean
+example : <some-proposition> := by
+  tac_1
+  tac_2
+  save
+  tac_3
+  ...
+```
+is equivalent to
+```lean
+example : <some-proposition> := by
+  checkpoint
+    tac_1
+    tac_2
+  tac_3
+  ...
+```
+
 * Remove support for `{}` annotation from inductive datatype contructors. This annotation was barely used, and we can control the binder information for parameter bindings using the new inductive family indices to parameter promotion. Example: the following declaration using `{}`
 ```lean
 inductive LE' (n : Nat) : Nat → Prop where