diff options
Diffstat (limited to 'doc')
7 files changed, 34 insertions, 6 deletions
diff --git a/doc/changelog/03-notations/11986-float-low-level-printing.rst b/doc/changelog/03-notations/11986-float-low-level-printing.rst new file mode 100644 index 0000000000..f3d85cadc6 --- /dev/null +++ b/doc/changelog/03-notations/11986-float-low-level-printing.rst @@ -0,0 +1,5 @@ +- **Added:** + Add flag ``Printing Float`` to print primitive floats as hexadecimal + instead of decimal values. This is included in ``Set Printing All``. + (`#11986 <https://github.com/coq/coq/pull/11986>`_, + by Pierre Roux). diff --git a/doc/changelog/07-commands-and-options/12295-master+fix12234-show-proof.rst b/doc/changelog/07-commands-and-options/12295-master+fix12234-show-proof.rst new file mode 100644 index 0000000000..259253ec79 --- /dev/null +++ b/doc/changelog/07-commands-and-options/12295-master+fix12234-show-proof.rst @@ -0,0 +1,4 @@ +- **Fixed:** + A printing bug in the presence of elimination principles with local definitions + (`#12295 <https://github.com/coq/coq/pull/12295>`_, + by Hugo Herbelin; fixes `#12233 <https://github.com/coq/coq/pull/12233>`_). diff --git a/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst b/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst new file mode 100644 index 0000000000..5b35090d7e --- /dev/null +++ b/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst @@ -0,0 +1,5 @@ +- **Changed:** + :cmd:Redirect now obeys the :opt:`Printing Width` and + :opt:`Printing Depth` flags. + (`#12358 <https://github.com/coq/coq/pull/12358>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/08-tools/12076-fix-5030.rst b/doc/changelog/08-tools/12076-fix-5030.rst new file mode 100644 index 0000000000..afb59b1cde --- /dev/null +++ b/doc/changelog/08-tools/12076-fix-5030.rst @@ -0,0 +1,4 @@ +- **Fixed:** + Fix #5030 (coqchk reports names from opaque modules as axioms) + (`#12076 <https://github.com/coq/coq/pull/12076>`_, + by Pierre Roux). diff --git a/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst b/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst new file mode 100644 index 0000000000..8a43f5af94 --- /dev/null +++ b/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst @@ -0,0 +1,4 @@ +- **Changed:** + The pretty-timed scripts and targets now print a newline at the end of their + tables, rather than creating text with no trailing newline (`#12368 + <https://github.com/coq/coq/pull/12368>`_, by Jason Gross). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5954ded67f..363148e2a0 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -147,7 +147,7 @@ Changes in 8.11+beta1 dropped when forcing a delayed opaque proof inside a polymorphic section. Also relaxes the nesting criterion for sections, as polymorphic sections can now appear inside a monomorphic one - (`#10664, <https://github.com/coq/coq/pull/10664>`_ by Pierre-Marie Pédrot). + (`#10664 <https://github.com/coq/coq/pull/10664>`_, by Pierre-Marie Pédrot). - **Changed:** Using ``SProp`` is now allowed by default, without needing to pass ``-allow-sprop`` or use :flag:`Allow StrictProp` (`#10811 @@ -476,7 +476,7 @@ Changes in 8.11+beta1 by Vincent Laporte). - **Removed:** Deprecated modules `Coq.ZArith.Zlogarithm` and `Coq.ZArith.Zsqrt_compat` - (`#9881 <https://github.com/coq/coq/pull/9811>`_, + (`#9811 <https://github.com/coq/coq/pull/9811>`_, by Vincent Laporte). .. _811Reals: @@ -690,7 +690,7 @@ Changes in 8.11.1 Bump official OCaml support and CI testing to 4.10.0 (`#11131 <https://github.com/coq/coq/pull/11131>`_, `#11123 <https://github.com/coq/coq/pull/11123>`_, - `#11102 <https://github.com/coq/coq/pull/11123>`_, + `#11102 <https://github.com/coq/coq/pull/11102>`_, by Emilio Jesus Gallego Arias, Jacques-Henri Jourdan, Guillaume Melquiond, and Guillaume Munch-Maccagnoni). @@ -1091,7 +1091,7 @@ Other changes in 8.10+beta1 e.g., a numeral notation whose parsing function outputs a proof of :g:`Nat.gcd x y = 1` will no longer fail to parse due to containing the constant :g:`Nat.gcd` in the parameter-argument of :g:`eq_refl`) - (`#9874 <https://github.com/coq/coq/pull/9840>`_, + (`#9874 <https://github.com/coq/coq/pull/9874>`_, closes `#9840 <https://github.com/coq/coq/issues/9840>`_ and `#9844 <https://github.com/coq/coq/issues/9844>`_, by Jason Gross). @@ -1107,7 +1107,7 @@ Other changes in 8.10+beta1 - Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar` (`#10061 <https://github.com/coq/coq/pull/10061>`_, - fixes `#9681 <http://github.com/coq/coq/pull/9681>`_, + fixes `#9681 <https://github.com/coq/coq/pull/9681>`_, by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin). - The `quote plugin diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 899173a83a..b2b68482ef 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -1062,11 +1062,17 @@ Floating-point constants are parsed and pretty-printed as (17-digit) decimal constants. This ensures that the composition :math:`\text{parse} \circ \text{print}` amounts to the identity. -.. warn:: The constant @numeral is not a binary64 floating-point value. A closest value will be used and unambiguously printed @numeral. [inexact-float,parsing] +.. warn:: The constant @numeral is not a binary64 floating-point value. A closest value @numeral will be used and unambiguously printed @numeral. [inexact-float,parsing] Not all decimal constants are floating-point values. This warning is generated when parsing such a constant (for instance ``0.1``). +.. flag:: Printing Float + + Turn this flag off (it is on by default) to deactivate decimal + printing of floating-point constants. They will then be printed + with an hexadecimal representation. + .. example:: .. coqtop:: all |