diff options
| author | Matthieu Sozeau | 2018-12-13 17:02:59 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-12-13 17:02:59 +0100 |
| commit | c5cd2cd4b2b50bb26aeb2b3ebe873c858df27efa (patch) | |
| tree | fbdc2e35e2c22d51ae2502fa2c42f83d7e1de9e3 /CHANGES.md | |
| parent | 9f4aa15eb94ec4b44a90d1e0832b1da04d857b63 (diff) | |
| parent | da4c116d650cc83171a8cd392307245cac826f73 (diff) | |
Merge PR #9117: Accept argument names for extra arguments with "extra scopes"
Diffstat (limited to 'CHANGES.md')
| -rw-r--r-- | CHANGES.md | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES.md b/CHANGES.md index 8cb71f19ea..4fafb9a18a 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -88,6 +88,8 @@ Vernacular commands - The `Automatic Introduction` option has been removed and is now the default. +- `Arguments` now accepts names for arguments provided with `extra_scopes`. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: |