Release notes for 8.12.

18 files changed, 0 insertions, 148 deletions

diff --git a/doc/changelog/08-tools/10592-coqdoc-details.rst b/doc/changelog/08-tools/10592-coqdoc-details.rst
deleted file mode 100644
index c5bdc1dbb0..0000000000
--- a/doc/changelog/08-tools/10592-coqdoc-details.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Added:**
-  A new documentation environment ``details`` to make certain portion
-  of a Coq document foldable.  See :ref:`coqdoc`
-  (`#10592 <https://github.com/coq/coq/pull/10592>`_,
-  by Thomas Letan).
diff --git a/doc/changelog/08-tools/11302-better-timing-scripts-options.rst b/doc/changelog/08-tools/11302-better-timing-scripts-options.rst
deleted file mode 100644
index 3b20bbf75d..0000000000
--- a/doc/changelog/08-tools/11302-better-timing-scripts-options.rst
+++ /dev/null
@@ -1,35 +0,0 @@
-- **Added:**
-  The ``make-both-single-timing-files.py`` script now accepts a
-  ``--fuzz=N`` parameter on the command line which determines how many
-  characters two lines may be offset in the "before" and "after"
-  timing logs while still being considered the same line.  When
-  invoking this script via the ``print-pretty-single-time-diff``
-  target in a ``Makefile`` made by ``coq_makefile``, you can set this
-  argument by passing ``TIMING_FUZZ=N`` to ``make`` (`#11302
-  <https://github.com/coq/coq/pull/11302>`_, by Jason Gross).
-
-- **Added:**
-  The ``make-one-time-file.py`` and ``make-both-time-files.py``
-  scripts now accept a ``--real`` parameter on the command line to
-  print real times rather than user times in the tables.  The
-  ``make-both-single-timing-files.py`` script accepts a ``--user``
-  parameter to use user times.  When invoking these scripts via the
-  ``print-pretty-timed`` or ``print-pretty-timed-diff`` or
-  ``print-pretty-single-time-diff`` targets in a ``Makefile`` made by
-  ``coq_makefile``, you can set this argument by passing
-  ``TIMING_REAL=1`` (to pass ``--real``) or ``TIMING_REAL=0`` (to pass
-  ``--user``) to ``make`` (`#11302
-  <https://github.com/coq/coq/pull/11302>`_, by Jason Gross).
-
-- **Added:**
-  Coq's build system now supports both ``TIMING_FUZZ``,
-  ``TIMING_SORT_BY``, and ``TIMING_REAL`` just like a ``Makefile``
-  made by ``coq_makefile`` (`#11302
-  <https://github.com/coq/coq/pull/11302>`_, by Jason Gross).
-
-- **Fixed:**
-  The various timing targets for Coq's standard library now correctly
-  display and label the "before" and "after" columns, rather than
-  mixing them up (`#11302 <https://github.com/coq/coq/pull/11302>`_
-  fixes `#11301 <https://github.com/coq/coq/issues/11301>`_, by Jason
-  Gross).
diff --git a/doc/changelog/08-tools/11409-mltop+deprecate_use.rst b/doc/changelog/08-tools/11409-mltop+deprecate_use.rst
deleted file mode 100644
index f4f110ed67..0000000000
--- a/doc/changelog/08-tools/11409-mltop+deprecate_use.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Removed:**
-  The `-load-ml-source` and `-load-ml-object` command line options
-  have been removed; their use was very limited, you can achieve the same adding
-  additional object files in the linking step or using a plugin
-  (`#11409 <https://github.com/coq/coq/pull/11409>`_, by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/08-tools/11523-coqdep+refactor2.rst b/doc/changelog/08-tools/11523-coqdep+refactor2.rst
deleted file mode 100644
index 3f93d60926..0000000000
--- a/doc/changelog/08-tools/11523-coqdep+refactor2.rst
+++ /dev/null
@@ -1,10 +0,0 @@
-- **Changed:**
-  Internal options and behavior of ``coqdep`` have changed. ``coqdep``
-  no longer works as a replacement for ``ocamldep``, thus ``.ml``
-  files are not supported as input. Also, several deprecated options
-  have been removed: ``-w``, ``-D``, ``-mldep``, ``-prefix``,
-  ``-slash``, and ``-dumpbox``. Passing ``-boot`` to ``coqdep`` will
-  not load any path by default now, ``-R/-Q`` should be used instead
-  (`#11523 <https://github.com/coq/coq/pull/11523>`_ and
-  `#11589 <https://github.com/coq/coq/pull/11589>`_,
-  by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/08-tools/11606-memory-in-timing-scripts.rst b/doc/changelog/08-tools/11606-memory-in-timing-scripts.rst
deleted file mode 100644
index e09c6ef3a3..0000000000
--- a/doc/changelog/08-tools/11606-memory-in-timing-scripts.rst
+++ /dev/null
@@ -1,25 +0,0 @@
-- **Added:**
-  The ``make-one-time-file.py`` and ``make-both-time-files.py``
-  scripts now include peak memory usage information in the tables (can
-  be turned off by the ``--no-include-mem`` command-line parameter),
-  and a ``--sort-by-mem`` parameter to sort the tables by memory
-  rather than time.  When invoking these scripts via the
-  ``print-pretty-timed`` or ``print-pretty-timed-diff`` targets in a
-  ``Makefile`` made by ``coq_makefile``, you can set this argument by
-  passing ``TIMING_INCLUDE_MEM=0`` (to pass ``--no-include-mem``) and
-  ``TIMING_SORT_BY_MEM=1`` (to pass ``--sort-by-mem``) to ``make``
-  (`#11606 <https://github.com/coq/coq/pull/11606>`_, by Jason Gross).
-
-- **Added:**
-  Coq's build system now supports both ``TIMING_INCLUDE_MEM`` and
-  ``TIMING_SORT_BY_MEM`` just like a ``Makefile`` made by
-  ``coq_makefile`` (`#11606 <https://github.com/coq/coq/pull/11606>`_,
-  by Jason Gross).
-
-- **Changed:**
-  The sorting order of the timing script ``make-both-time-files.py``
-  and the target ``print-pretty-timed-diff`` is now deterministic even
-  when the sorting order is ``absolute`` or ``diff``; previously the
-  relative ordering of two files with identical times was
-  non-deterministic (`#11606
-  <https://github.com/coq/coq/pull/11606>`_, by Jason Gross).
diff --git a/doc/changelog/08-tools/11617-toplevel+boot.rst b/doc/changelog/08-tools/11617-toplevel+boot.rst
deleted file mode 100644
index 49dd0ee2d8..0000000000
--- a/doc/changelog/08-tools/11617-toplevel+boot.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Added:**
-  New ``coqc`` / ``coqtop`` option ``-boot`` that will not bind the
-  `Coq` library prefix by default
-  (`#11617 <https://github.com/coq/coq/pull/11617>`_,
-  by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/08-tools/11851-coqc-flags-fix.rst b/doc/changelog/08-tools/11851-coqc-flags-fix.rst
deleted file mode 100644
index ff736641b4..0000000000
--- a/doc/changelog/08-tools/11851-coqc-flags-fix.rst
+++ /dev/null
@@ -1,9 +0,0 @@
-- **Changed:**
-  The order in which the require flags `-ri`, `-re`, `-rfrom`, etc.
-  and the option flags `-set`, `-unset` are given now matters.  In
-  particular, it is now possible to interleave the loading of plugins
-  and the setting of options by choosing the right order for these
-  flags.  The load flags `-l` and `-lv` are still processed afterward
-  for now (`#11851 <https://github.com/coq/coq/pull/11851>`_ and
-  `#12097 <https://github.com/coq/coq/pull/12097>`_,
-  by Lasse Blaauwbroek).
diff --git a/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst
deleted file mode 100644
index affb685fcb..0000000000
--- a/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Removed:**
-  Confusingly-named and deprecated since 8.11 `-require` option.
-  Use the equivalent `-require-import` instead
-  (`#12005 <https://github.com/coq/coq/pull/12005>`_,
-  by Théo Zimmermann).
diff --git a/doc/changelog/08-tools/12006-issue5632.rst b/doc/changelog/08-tools/12006-issue5632.rst
deleted file mode 100644
index 162d56b1b6..0000000000
--- a/doc/changelog/08-tools/12006-issue5632.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  ``Makefile`` generated by ``coq_makefile`` erases ``.lia.cache`` and ``.nia.cache`` by ``make cleanall``.
-  (`#12006 <https://github.com/coq/coq/pull/12006>`_,
-  by Olivier Laurent).
diff --git a/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst b/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst
deleted file mode 100644
index 5c4ef82b8b..0000000000
--- a/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  Definitions in coqdoc link to themselves, giving access in html to their own url
-  (`#12026 <https://github.com/coq/coq/pull/12026>`_,
-  by Hugo Herbelin; granting `#7093 <https://github.com/coq/coq/pull/7093>`_).
diff --git a/doc/changelog/08-tools/12027-master+fix3415-coqdoc-record.rst b/doc/changelog/08-tools/12027-master+fix3415-coqdoc-record.rst
deleted file mode 100644
index ae9b69e592..0000000000
--- a/doc/changelog/08-tools/12027-master+fix3415-coqdoc-record.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Fixed:**
-  Fields of a record tuple now link in coqdoc to their definition
-  (`#12027 <https://github.com/coq/coq/pull/12027>`_, fixes
-  `#3415 <https://github.com/coq/coq/issues/3415>`_,
-  by Hugo Herbelin; ).
diff --git a/doc/changelog/08-tools/12033-master+coqdoc-fix7697-passing-binders-location.rst b/doc/changelog/08-tools/12033-master+coqdoc-fix7697-passing-binders-location.rst
deleted file mode 100644
index af0d28305a..0000000000
--- a/doc/changelog/08-tools/12033-master+coqdoc-fix7697-passing-binders-location.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Added:**
-  Add hyperlinks on bound variables for coqdoc
-  (`#12033 <https://github.com/coq/coq/pull/12033>`_,
-  by Hugo Herbelin; it incidentally fixes
-  `#7697 <https://github.com/coq/coq/pull/7697>`_).
diff --git a/doc/changelog/08-tools/12037-coqdoc-preformatted.rst b/doc/changelog/08-tools/12037-coqdoc-preformatted.rst
deleted file mode 100644
index bf65719516..0000000000
--- a/doc/changelog/08-tools/12037-coqdoc-preformatted.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Fixed:**
-  ``coqdoc`` now reports the location of a mismatched opening ``[[`` instead of
-  throwing an uninformative exception.
-  (`#12037 <https://github.com/coq/coq/pull/12037>`_,
-  fixes `#9670 <https://github.com/coq/coq/issues/9670>`_,
-  by Lysxia).
diff --git a/doc/changelog/08-tools/12076-fix-5030.rst b/doc/changelog/08-tools/12076-fix-5030.rst
deleted file mode 100644
index afb59b1cde..0000000000
--- a/doc/changelog/08-tools/12076-fix-5030.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **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/12091-master+coqdoc-css-target.rst b/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst
deleted file mode 100644
index f6af5d40e8..0000000000
--- a/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  ``Coqdoc``: Highlighting of the exact position of the target of links
-  (`#12091 <https://github.com/coq/coq/pull/12091>`_,
-  by Hugo Herbelin).
diff --git a/doc/changelog/08-tools/12126-adjust-timed-name.rst b/doc/changelog/08-tools/12126-adjust-timed-name.rst
deleted file mode 100644
index c305b384d9..0000000000
--- a/doc/changelog/08-tools/12126-adjust-timed-name.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-- **Changed:**
-  The output of ``make TIMED=1`` (and therefore the timing targets
-  such as ``print-pretty-timed`` and ``print-pretty-timed-diff``) now
-  displays the full name of the output file being built, rather than
-  the stem of the rule (which was usually the filename without the
-  extension, but in general could be anything for user-defined rules
-  involving ``%``) (`#12126
-  <https://github.com/coq/coq/pull/12126>`_, by Jason Gross).
diff --git a/doc/changelog/08-tools/12211-time-ocaml.rst b/doc/changelog/08-tools/12211-time-ocaml.rst
deleted file mode 100644
index 7ff68cc495..0000000000
--- a/doc/changelog/08-tools/12211-time-ocaml.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Changed:**
-  When passing ``TIMED=1`` to ``make`` with either Coq's own makefile
-  or a ``coq_makefile``\-made makefile, timing information is now
-  printed for OCaml files as well (`#12211
-  <https://github.com/coq/coq/pull/12211>`_, by Jason Gross).
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
deleted file mode 100644
index 8a43f5af94..0000000000
--- a/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **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).