diff options
| author | Pierre-Marie Pédrot | 2021-03-05 19:04:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-05 19:04:27 +0100 |
| commit | aacf8f1756fa5a289f27485a1951392505edfc53 (patch) | |
| tree | ab18d66b36858bb17dff02b041e9b5817cdb9a5c /doc | |
| parent | b016348348f8b2dfaaf19c3a46436261a0ebde42 (diff) | |
| parent | 303941d805efe6d02273afa099fac74cc0efbf90 (diff) | |
Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12)
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/03-notations/13842-remove-decimal.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 6 |
2 files changed, 3 insertions, 6 deletions
diff --git a/doc/changelog/03-notations/13842-remove-decimal.rst b/doc/changelog/03-notations/13842-remove-decimal.rst new file mode 100644 index 0000000000..4bc26ef6a8 --- /dev/null +++ b/doc/changelog/03-notations/13842-remove-decimal.rst @@ -0,0 +1,3 @@ +- **Removed:** + Remove decimal-only number notations which were deprecated in 8.12. + (`#13842 <https://github.com/coq/coq/pull/13842>`_, by Pierre Roux). diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 03571ad680..557ef10555 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1726,12 +1726,6 @@ Number notations * :n:`@qualid__type -> Number.number` * :n:`@qualid__type -> option Number.number` - .. deprecated:: 8.12 - Number notations on :g:`Decimal.uint`, :g:`Decimal.int` and - :g:`Decimal.decimal` are replaced respectively by number - notations on :g:`Number.uint`, :g:`Number.int` and - :g:`Number.number`. - When parsing, the application of the parsing function :n:`@qualid__parse` to the number will be fully reduced, and universes of the resulting term will be refreshed. |