From 94132f40eb81ed3249c4d5f32f6d7aa356d38847 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 12 Sep 2020 08:54:17 +0200 Subject: Add changelog --- .../12218-numeral-notations-non-inductive.rst | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst (limited to 'doc') 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 ` and :ref:`String Notation + ` commands now + support parameterized inductive and non inductive types + (`#12218 `_, + fixes `#12035 `_, + by Pierre Roux, review by Jason Gross and Jim Fehrle for the + reference manual). -- cgit v1.2.3