diff options
Diffstat (limited to 'doc/changelog/01-kernel')
4 files changed, 10 insertions, 6 deletions
diff --git a/doc/changelog/01-kernel/09867-floats.rst b/doc/changelog/01-kernel/09867-floats.rst index 56b5fc747a..cae4dbb335 100644 --- a/doc/changelog/01-kernel/09867-floats.rst +++ b/doc/changelog/01-kernel/09867-floats.rst @@ -1,4 +1,5 @@ -- A built-in support of floating-point arithmetic was added, allowing +- **Added:** + A built-in support of floating-point arithmetic, allowing one to devise efficient reflection tactics involving numerical computation. Primitive floats are added in the language of terms, following the binary64 format of the IEEE 754 standard, and the diff --git a/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.rst b/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.rst index e0573a2c74..84060ddf29 100644 --- a/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.rst +++ b/doc/changelog/01-kernel/10439-uniform-opaque-seff-handling.rst @@ -1,4 +1,5 @@ -- Internal definitions generated by abstract-like tactics are now inlined - inside universe Qed-terminated polymorphic definitions, similarly to what +- **Changed:** + Internal definitions generated by :tacn:`abstract`\-like tactics are now inlined + inside universe :cmd:`Qed`\-terminated polymorphic definitions, similarly to what happens for their monomorphic counterparts, (`#10439 <https://github.com/coq/coq/pull/10439>`_, by Pierre-Marie Pédrot). diff --git a/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst b/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst index bac08d12ea..5d224797d4 100644 --- a/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst +++ b/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst @@ -1,6 +1,7 @@ -- Section data is now part of the kernel. Solves a soundness issue +- **Fixed:** + Section data is now part of the kernel. Solves a soundness issue in interactive mode where global monomorphic universe constraints would be 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). diff --git a/doc/changelog/01-kernel/10811-sprop-default-on.rst b/doc/changelog/01-kernel/10811-sprop-default-on.rst index 349c44c205..2c008fb5d3 100644 --- a/doc/changelog/01-kernel/10811-sprop-default-on.rst +++ b/doc/changelog/01-kernel/10811-sprop-default-on.rst @@ -1,3 +1,4 @@ -- Using ``SProp`` is now allowed by default, without needing to pass +- **Changed:** + Using ``SProp`` is now allowed by default, without needing to pass ``-allow-sprop`` or use :flag:`Allow StrictProp` (`#10811 <https://github.com/coq/coq/pull/10811>`_, by Gaëtan Gilbert). |