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 91763ba35c..267a2e2d32 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -52,6 +52,9 @@ Vernacular commands - `Combined Scheme` can now work when inductive schemes are generated in sort `Type`. It used to be limited to sort `Prop`. +- Binders for an `Instance` now act more like binders for a `Theorem`. + Names may not be repeated, and may not overlap with section variable names. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: |