Release notes for 8.12.

9 files changed, 0 insertions, 53 deletions

diff --git a/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst b/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst
deleted file mode 100644
index 57bce7e4f6..0000000000
--- a/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-- **Changed:**
-  Warn when manual implicit arguments are used in unexpected positions
-  of a term (e.g. in `Check id (forall {x}, x)`) or when a implicit
-  argument name is shadowed (e.g. in `Check fun f : forall {x:nat}
-  {x}, nat => f`)
-  (`#10202 <https://github.com/coq/coq/pull/10202>`_,
-  by Hugo Herbelin).
diff --git a/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst b/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst
deleted file mode 100644
index 70c57c718f..0000000000
--- a/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-- **Added:**
-  :cmd:`Arguments` now supports setting
-  implicit an anonymous argument, as e.g. in :g:`Arguments id {A} {_}`.
-  (`#11098 <https://github.com/coq/coq/pull/11098>`_,
-  by Hugo Herbelin, fixes `#4696
-  <https://github.com/coq/coq/pull/4696>`_, `#5173
-  <https://github.com/coq/coq/pull/5173>`_, `#9098
-  <https://github.com/coq/coq/pull/9098>`_).
diff --git a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst
deleted file mode 100644
index 768ef68339..0000000000
--- a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Added:**
-  Syntax for non-maximal implicit arguments in definitions and terms using
-  square brackets. The syntax is ``[x : A]``, ``[x]``, ```[A]``
-  to be consistent with the command :cmd:`Arguments`.
-  (`#11235 <https://github.com/coq/coq/pull/11235>`_,
-  by SimonBoulier).
diff --git a/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst b/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst
deleted file mode 100644
index 51818c666b..0000000000
--- a/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Added:**
-  :cmd:`Implicit Types` are now taken into account for printing. To inhibit it,
-  unset the :flag:`Printing Use Implicit Types` flag
-  (`#11261 <https://github.com/coq/coq/pull/11261>`_,
-  by Hugo Herbelin, granting `#10366 <https://github.com/coq/coq/pull/10366>`_).
diff --git a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst
deleted file mode 100644
index 66139f76e1..0000000000
--- a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Changed:**
-  The warning raised when a trailing implicit is declared to be non-maximally
-  inserted (with the command :cmd:`Arguments`) has been turned into an error.
-  This was deprecated since Coq 8.10
-  (`#11368 <https://github.com/coq/coq/pull/11368>`_,
-  by SimonBoulier).
diff --git a/doc/changelog/02-specification-language/11579-inductive-params.rst b/doc/changelog/02-specification-language/11579-inductive-params.rst
deleted file mode 100644
index 28bc8e9592..0000000000
--- a/doc/changelog/02-specification-language/11579-inductive-params.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-- **Fixed:**
-  More robust and expressive treatment of implicit inductive
-  parameters in inductive declarations (`#11579
-  <https://github.com/coq/coq/pull/11579>`_, by Maxime Dénès, Gaëtan
-  Gilbert and Jasper Hugunin; fixes `#7253
-  <https://github.com/coq/coq/pull/7253>`_ and `#11585
-  <https://github.com/coq/coq/pull/11585>`_)
diff --git a/doc/changelog/02-specification-language/11600-uniform-syntax.rst b/doc/changelog/02-specification-language/11600-uniform-syntax.rst
deleted file mode 100644
index b95bad2eb8..0000000000
--- a/doc/changelog/02-specification-language/11600-uniform-syntax.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Added:**
-  New syntax :g:`Inductive Acc A R | x : Prop := ...` to specify which
-  parameters of an inductive are uniform.
-  See :ref:`parametrized-inductive-types`
-  (`#11600 <https://github.com/coq/coq/pull/11600>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/02-specification-language/12121-master+fix11903-warn-non-truly-fixpoint.rst b/doc/changelog/02-specification-language/12121-master+fix11903-warn-non-truly-fixpoint.rst
deleted file mode 100644
index d69a94205f..0000000000
--- a/doc/changelog/02-specification-language/12121-master+fix11903-warn-non-truly-fixpoint.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Added:**
-  New warning on using :cmd:`Fixpoint` or :cmd:`CoFixpoint` for
-  definitions which are not recursive
-  (`#12121 <https://github.com/coq/coq/pull/12121>`_,
-  by Hugo Herbelin)
diff --git a/doc/changelog/02-specification-language/12323-master+fix12322-anomaly-implicit-binder-factorization.rst b/doc/changelog/02-specification-language/12323-master+fix12322-anomaly-implicit-binder-factorization.rst
deleted file mode 100644
index e5ec865b15..0000000000
--- a/doc/changelog/02-specification-language/12323-master+fix12322-anomaly-implicit-binder-factorization.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Fixed:**
-  Anomaly possibly raised when printing binders with implicit types
-  (`#12323 <https://github.com/coq/coq/pull/12323>`_,
-  by Hugo Herbelin; fixes `#12322 <https://github.com/coq/coq/pull/12322>`_).