diff --git a/doc/changes.md b/doc/changes.md index c3a41e9a27..866a4f3936 100644 --- a/doc/changes.md +++ b/doc/changes.md @@ -88,6 +88,8 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/ * Removed the redundant keywords `take` (replace with `assume`) and `suppose` (replace with the new anonymous `assume :`) +* Universes `max u v + 1` and `imax u v + 1` are now parsed as `(max u v) + 1` and `(imax u v) + 1`. + *API name changes* * `list.dropn` => `list.drop`