fix(doc/changes): describe fallout from parameterized user attributes
@kha This was an unexpected breakage resulting from #1809.
This commit is contained in:
parent
88cd294a09
commit
b59d2771ea
1 changed files with 2 additions and 0 deletions
|
|
@ -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`
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue