diff options
| author | Pierre Roux | 2020-09-12 08:54:17 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-11-05 00:20:53 +0100 |
| commit | 94132f40eb81ed3249c4d5f32f6d7aa356d38847 (patch) | |
| tree | a44987538ea59271b71c662f0fb9e1bfbb983ada | |
| parent | 36ac26532028bfc6f84e4dfc849b51f42a3d8286 (diff) | |
Add changelog
| -rw-r--r-- | doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst b/doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst new file mode 100644 index 0000000000..5ea37e7494 --- /dev/null +++ b/doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst @@ -0,0 +1,19 @@ +- **Deprecated** + ``Numeral.v`` is deprecated, please use ``Number.v`` instead. +- **Changed** + Rational and real constants are parsed differently. + The exponent is now encoded separately from the fractional part + using ``Z.pow_pos``. This way, parsing large exponents can no longer + blow up and constants are printed in a form closer to the one they + were parsed (i.e., ``102e-2`` is reprinted as such and not ``1.02``). +- **Removed** + OCaml parser and printer for real constants have been removed. + Real constants are now handled with proven Coq code. +- **Added:** + :ref:`Number Notation <number-notations>` and :ref:`String Notation + <string-notations>` commands now + support parameterized inductive and non inductive types + (`#12218 <https://github.com/coq/coq/pull/12218>`_, + fixes `#12035 <https://github.com/coq/coq/issues/12035>`_, + by Pierre Roux, review by Jason Gross and Jim Fehrle for the + reference manual). |