diff options
Diffstat (limited to 'CHANGES.md')
| -rw-r--r-- | CHANGES.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/CHANGES.md b/CHANGES.md index 1a0b53f84a..98440a8959 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -114,7 +114,7 @@ Vernacular commands avoid conflicts with explicitly named binders. - Computation of implicit arguments now properly handles local definitions in the - binders for an `Instance`. + binders for an `Instance`, and can be mixed with implicit binders `{x : T}`. - `Declare Instance` now requires an instance name. |