From 39e3201c01b1a8baec279ccdc7a8acb3a341c3dd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 1 Apr 2021 11:18:44 +0200 Subject: changelog for 8.13.2 --- doc/changelog/01-kernel/14004-vm-array-set.rst | 5 ---- doc/changelog/01-kernel/14007-fix-14006.rst | 7 ------ .../04-tactics/14012-ltac2-array-init.rst | 4 ---- doc/sphinx/changes.rst | 27 ++++++++++++++++++++++ 4 files changed, 27 insertions(+), 16 deletions(-) delete mode 100644 doc/changelog/01-kernel/14004-vm-array-set.rst delete mode 100644 doc/changelog/01-kernel/14007-fix-14006.rst delete mode 100644 doc/changelog/04-tactics/14012-ltac2-array-init.rst diff --git a/doc/changelog/01-kernel/14004-vm-array-set.rst b/doc/changelog/01-kernel/14004-vm-array-set.rst deleted file mode 100644 index f90d611f84..0000000000 --- a/doc/changelog/01-kernel/14004-vm-array-set.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Crash when using :tacn:`vm_compute` on an irreducible ``PArray.set`` - (`#14005 `_, - fixes `#13998 `_, - by Guillaume Melquiond). diff --git a/doc/changelog/01-kernel/14007-fix-14006.rst b/doc/changelog/01-kernel/14007-fix-14006.rst deleted file mode 100644 index 6765768295..0000000000 --- a/doc/changelog/01-kernel/14007-fix-14006.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Fixed:** - Never store persistent arrays as VM / native structured values. - This could be used to make vo marshalling crash, and probably - breaking some other invariants of the kernel - (`#14007 `_, - fixes `#14006 `_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/04-tactics/14012-ltac2-array-init.rst b/doc/changelog/04-tactics/14012-ltac2-array-init.rst deleted file mode 100644 index c79fc7e29a..0000000000 --- a/doc/changelog/04-tactics/14012-ltac2-array-init.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - Ltac2 ``Array.init`` no longer incurs exponential overhead when used - recursively (`#14012 `_, fixes `#14011 - `_, by Jason Gross). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 4f3ee2dcaf..6b4bcad4f3 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -721,6 +721,33 @@ CoqIDE (`#13870 `_, by Guillaume Melquiond). +Changes in 8.13.2 +~~~~~~~~~~~~~~~~~ + +Kernel +^^^^^^ + +- **Fixed:** + Crash when using :tacn:`vm_compute` on an irreducible ``PArray.set`` + (`#14005 `_, + fixes `#13998 `_, + by Guillaume Melquiond). +- **Fixed:** + Never store persistent arrays as VM / native structured values. + This could be used to make vo marshalling crash, and probably + breaking some other invariants of the kernel + (`#14007 `_, + fixes `#14006 `_, + by Pierre-Marie Pédrot). + +Tactics +^^^^^^^ + +- **Fixed:** + Ltac2 ``Array.init`` no longer incurs exponential overhead when used + recursively (`#14012 `_, fixes `#14011 + `_, by Jason Gross). + Version 8.12 ------------ -- cgit v1.2.3 From 24c7980f64201510966dbb5169028bc9deccfce4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 1 Apr 2021 12:59:45 +0200 Subject: Update doc/sphinx/changes.rst Co-authored-by: Théo Zimmermann --- doc/sphinx/changes.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 6b4bcad4f3..74aa6e21ce 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -740,7 +740,7 @@ Kernel fixes `#14006 `_, by Pierre-Marie Pédrot). -Tactics +Tactic language ^^^^^^^ - **Fixed:** -- cgit v1.2.3 From c4262d1bea90e34adf429b891b2f8be259851949 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 1 Apr 2021 14:36:50 +0200 Subject: Update doc/sphinx/changes.rst Co-authored-by: Théo Zimmermann --- doc/sphinx/changes.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 74aa6e21ce..bf8174f246 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -741,7 +741,7 @@ Kernel by Pierre-Marie Pédrot). Tactic language -^^^^^^^ +^^^^^^^^^^^^^^^^ - **Fixed:** Ltac2 ``Array.init`` no longer incurs exponential overhead when used -- cgit v1.2.3