diff options
Diffstat (limited to 'doc/changelog/03-notations/13965-syndef-principal-scope.rst')
| -rw-r--r-- | doc/changelog/03-notations/13965-syndef-principal-scope.rst | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/doc/changelog/03-notations/13965-syndef-principal-scope.rst b/doc/changelog/03-notations/13965-syndef-principal-scope.rst new file mode 100644 index 0000000000..448dbbe3c7 --- /dev/null +++ b/doc/changelog/03-notations/13965-syndef-principal-scope.rst @@ -0,0 +1,12 @@ +- **Added:** + Let the user specify a scope for abbreviation arguments, e.g. + ``Notation abbr X := t (X in scope my_scope)``. + (`#13965 <https://github.com/coq/coq/pull/13965>`_, + by Enrico Tassi). +- **Changed:** + The error ``Argument X was previously inferred to be in scope + XXX_scope but is here used in YYY_scope.`` is now the warning + ``[inconsistent-scopes,syntax]`` and can be silenced by + specifying the scope of the argument + (`#13965 <https://github.com/coq/coq/pull/13965>`_, + by Enrico Tassi). |