diff --git a/CHANGELOG.md b/CHANGELOG.md index 9c8723765fbc998c9be8ce2702685112a1c4b2bf..2207c555923af5c1ffcad21e2eb1dbcdcfa24046 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`).