diff options
Diffstat (limited to 'CHANGES.md')
| -rw-r--r-- | CHANGES.md | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/CHANGES.md b/CHANGES.md index 6789bc038e..ae67eb5d1b 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -93,6 +93,9 @@ Vernacular commands - The naming scheme for anonymous binders in a `Theorem` has changed to avoid conflicts with explicitly named binders. +- Computation of implicit arguments now properly handles local definitions in the + binders for an `Instance`. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: |