From 1ecabad29170661d74b2afb119a35aec8e833398 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com> Date: Wed, 28 Jul 2021 14:14:53 +0200 Subject: [PATCH] Changelog --- CHANGELOG.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 87cf0e59..9314f0c3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -151,6 +151,8 @@ API-breaking change is listed. `map_filter_singleton_False`, `map_filter_comm`, `map_union_least`, `map_subseteq_difference_l`, `insert_difference`, `insert_difference'`, `difference_insert`, `difference_insert_subseteq`. (by Hai Dang) +- Tweak reduction on `gset`, so that `cbn` matches the behavior by `simpl` and + does not unfold `gset` operations. (by Paolo G. Giarrusso, BedRock Systems) 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