From b59d2771ea370fd9a3801f512738c67175f04498 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 6 Sep 2017 08:39:30 +0200 Subject: [PATCH] fix(doc/changes): describe fallout from parameterized user attributes @kha This was an unexpected breakage resulting from #1809. --- doc/changes.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/changes.md b/doc/changes.md index d802d99315..886d7b94ac 100644 --- a/doc/changes.md +++ b/doc/changes.md @@ -137,6 +137,8 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/ `⟨h1, h2⟩`. This change is motivated by the previous one. Without it, `and.intro h1 h2` would be pretty printed as `{left := h1, right := h2}`. +* User attributes can no longer be set with `set_basic_attribute`. You need to use `user_attribute.set_param` now. + *API name changes* * `list.dropn` => `list.drop`