diff options
| author | Pierre-Marie Pédrot | 2020-01-22 18:09:29 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-01-22 18:09:29 +0100 |
| commit | 661f010e0b2b8cee2e6bab0cc2b72fb19416cb84 (patch) | |
| tree | 443d8f5c8952301d430a8ad6ab148c363059b5b8 /doc/changelog/01-kernel | |
| parent | 3d85312403d6b985115e7f733a3141315e11e56c (diff) | |
| parent | 68421494cbd8d9e2bc8ab2482ee6f34a057b157a (diff) | |
Merge PR #11372: Changelog for 8.11.0.
Reviewed-by: ppedrot
Diffstat (limited to 'doc/changelog/01-kernel')
| -rw-r--r-- | doc/changelog/01-kernel/11081-native-cleanup.rst | 4 | ||||
| -rw-r--r-- | doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst | 4 | ||||
| -rw-r--r-- | doc/changelog/01-kernel/11422-Setplus2.rst | 4 |
3 files changed, 0 insertions, 12 deletions
diff --git a/doc/changelog/01-kernel/11081-native-cleanup.rst b/doc/changelog/01-kernel/11081-native-cleanup.rst deleted file mode 100644 index b3e3a78b96..0000000000 --- a/doc/changelog/01-kernel/11081-native-cleanup.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** the native compilation (:tacn:`native_compute`) now - creates a directory to contain temporary files instead of putting - them in the root of the system temporary directory. (`#11081 - <https://github.com/coq/coq/pull/11081>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst b/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst deleted file mode 100644 index 8c84648aa7..0000000000 --- a/doc/changelog/01-kernel/11361-fix-11360-discharge-template-param-var.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** `#11360 <https://github.com/issues/11360>`_ - Broken section closing when a template polymorphic inductive type depends on - a section variable through its parameters (`#11361 - <https://github.com/coq/coq/pull/11361>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/01-kernel/11422-Setplus2.rst b/doc/changelog/01-kernel/11422-Setplus2.rst deleted file mode 100644 index cc174358cc..0000000000 --- a/doc/changelog/01-kernel/11422-Setplus2.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - The type of :g:`Set+1` would be computed to be itself, leading to a proof of False. - (`#11422 <https://github.com/coq/coq/pull/11422>`_, - by Gaëtan Gilbert). |