diff --git a/CHANGELOG.md b/CHANGELOG.md index 0399e0d88846ed54c2db3e1e33c52b40b297a1ab..9a9c58eb7d687d07bd956c6b37c40f17e99b6be7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -53,6 +53,7 @@ Coq 8.8 and 8.9 are no longer supported. are used for `A → B1` and `A → B2` variants of `A ↔ B1 ∧ B2` lemmas. - Rename `Forall_Forall2` → `Forall_Forall2_diag` to be consistent with the names for big operators in Iris. +- Add `eunify` tactic that lifts Coq's `unify` tactic to `open_constr`. The following `sed` script should perform most of the renaming (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):