From f09470bb54857c2e14ead19c01f8775da20defae Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 29 Jun 2021 13:20:22 +0200
Subject: [PATCH] changelog

---
 CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9c872376..2207c555 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -109,6 +109,8 @@ API-breaking change is listed.
   is consistent with `delete_insert`.
 - Fix statement of `sum_inhabited_r`. (by Paolo G. Giarrusso)
 - Make `done` work on goals of the form `is_Some`.
+- Add `mk_evar` tactic to generate evars (intended as a more useful replacement
+  for Coq's `evar` tactic).
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
-- 
GitLab