diff options
| author | Théo Zimmermann | 2019-10-22 11:20:07 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-11-28 10:04:32 +0100 |
| commit | fbdde37d9d7d2fce7fe9b7035ad0e8efa7799dff (patch) | |
| tree | a6d68fd1a86a6e6adbae7d6dcf0e76f09425efe5 /doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst | |
| parent | 570018fe2c37eee1f87d509037162768bffe6366 (diff) | |
[changelog] Add types to changelog entries.
Types of changes are defined in the list defined by Keep a Changelog
1.0.0 (https://keepachangelog.com/en/1.0.0/):
- Added
- Changed
- Deprecated
- Fixed
- Removed
We exclude the type Security for now, even for soundness fixes,
because the process of handling security vulnerabilities is different
from anything we follow right now.
Diffstat (limited to 'doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst')
| -rw-r--r-- | doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst | 5 |
1 files changed, 3 insertions, 2 deletions
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). |