diff options
| author | Matthieu Sozeau | 2020-12-01 15:05:35 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2020-12-03 16:03:37 +0100 |
| commit | e9b3040326632589d811253e91de4f27c9cf70b4 (patch) | |
| tree | 10eb35ed61be4000b11522f6f5c2ba881bcee66f /doc/sphinx | |
| parent | 554a3b171e33a649c65a509046387b86615b4348 (diff) | |
Changes without PR references fixes
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/changes.rst | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 0626f240fd..c9968a64b2 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -292,15 +292,21 @@ Notations by Hugo Herbelin). - **Deprecated** ``Numeral.v`` is deprecated, please use ``Number.v`` instead. + (`#12218 <https://github.com/coq/coq/pull/12218>`_, + by Pierre Roux). - **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 in which they were parsed (i.e., ``102e-2`` is reprinted as such and not ``1.02``). + (`#12218 <https://github.com/coq/coq/pull/12218>`_, + by Pierre Roux). - **Removed** OCaml parser and printer for real constants have been removed. Real constants are now handled with proven Coq code. + (`#12218 <https://github.com/coq/coq/pull/12218>`_, + by Pierre Roux). - **Added:** :ref:`Number Notation <number-notations>` and :ref:`String Notation <string-notations>` commands now @@ -543,8 +549,8 @@ Commands and options by Pierre-Marie Pédrot). - **Changed:** The :attr:`export` locality can now be used for all Hint commands, - including :tacn:`Hint Cut`, :tacn:`Hint Mode`, :tacn:`Hint Transparent` / `Opaque` and - :tacn:`Remove Hints` + including :cmd:`Hint Cut`, :cmd:`Hint Mode`, :cmd:`Hint Transparent` / `Opaque` and + :cmd:`Remove Hints` (`#13388 <https://github.com/coq/coq/pull/13388>`_, by Pierre-Marie Pédrot). |