diff options
| author | Gaëtan Gilbert | 2019-10-30 15:41:41 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-30 17:57:38 +0100 |
| commit | a6e7775b67fe8f82d31d16777559940d6675c94d (patch) | |
| tree | adf07705cdfd445e7f8bfed6e2eb0cb55d83a349 /doc | |
| parent | dbcdc4e53758339d2a7eb96d19fbcffeb143154d (diff) | |
Implement the unsupported attribute error using the warning system
This means we can disable it to ignore unsupported attributes. For
instance this would be useful if we change some behaviour of `Cmd` and add an
attribute `att` to restore the old behaviour, then `#[att] Cmd` is
backwards compatible if the warning is disabled.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 5 |
2 files changed, 8 insertions, 0 deletions
diff --git a/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst new file mode 100644 index 0000000000..43a748b365 --- /dev/null +++ b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst @@ -0,0 +1,3 @@ +- The unsupported attribute error is now an error-by-default warning, + meaning it can be disabled (`#10997 + <https://github.com/coq/coq/pull/10997>`_, by Gaëtan Gilbert). diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index ae9d284661..dd65d4aeb3 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1556,6 +1556,11 @@ the following attributes names are recognized: now foo. Abort. +.. warn:: Unsupported attribute + + This warning is an error by default. It is caused by using a + command with some attribute it does not understand. + .. [1] This is similar to the expression “*entry* :math:`\{` sep *entry* :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry* |