Release notes for 8.12.

11 files changed, 0 insertions, 76 deletions

diff --git a/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst b/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst
deleted file mode 100644
index a8d4fc6ed2..0000000000
--- a/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Fixed:**
-  Different interpretations in different scopes of the same notation
-  string can now be associated to different printing formats (`#10832
-  <https://github.com/coq/coq/pull/10832>`_, by Hugo Herbelin,
-  fixes `#6092 <https://github.com/coq/coq/issues/6092>`_
-  and `#7766 <https://github.com/coq/coq/issues/7766>`_).
diff --git a/doc/changelog/03-notations/11113-remove-compat.rst b/doc/changelog/03-notations/11113-remove-compat.rst
deleted file mode 100644
index 3bcdd3dd6f..0000000000
--- a/doc/changelog/03-notations/11113-remove-compat.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Removed:** deprecated ``compat`` modifier of :cmd:`Notation`
-  and :cmd:`Infix` commands
-  (`#11113 <https://github.com/coq/coq/pull/11113>`_,
-  by Théo Zimmermann, with help from Jason Gross).
diff --git a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
deleted file mode 100644
index eeb4c755f6..0000000000
--- a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
+++ /dev/null
@@ -1,17 +0,0 @@
-- **Fixed:** Parsing and printing consistently handle inheritance of implicit
-  arguments in notations. With the exception of notations of
-  the form :n:`Notation @string := @@qualid` and :n:`Notation @ident := @@qualid` which
-  inhibit implicit arguments, all notations binding a partially
-  applied constant, as e.g. in :n:`Notation @string := (@qualid {+ @arg })`,
-  or :n:`Notation @string := (@@qualid {+ @arg })`, or
-  :n:`Notation @ident := (@qualid {+ @arg })`, or :n:`Notation @ident
-  := (@@qualid {+ @arg })`, inherit the remaining implicit arguments
-  (`#11120 <https://github.com/coq/coq/pull/11120>`_, by Hugo
-  Herbelin, fixing `#4690 <https://github.com/coq/coq/pull/4690>`_ and
-  `#11091 <https://github.com/coq/coq/pull/11091>`_).
-
-- **Changed:** Notation scopes are now always inherited in
-  notations binding a partially applied constant, including for
-  notations binding an expression of the form :n:`@@qualid`. The latter was
-  not the case beforehand
-  (part of `#11120 <https://github.com/coq/coq/pull/11120>`_).
diff --git a/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst b/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst
deleted file mode 100644
index f377b53ae2..0000000000
--- a/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-- **Changed:**
-  The printing algorithm now interleaves search for notations and removal of coercions
-  (`#11172 <https://github.com/coq/coq/pull/11172>`_, by Hugo Herbelin).
diff --git a/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst b/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst
deleted file mode 100644
index 1d94cbf21b..0000000000
--- a/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Fixed:**
-  Notations in onlyprinting mode do not uselessly reserve parsing keywords
-  (`#11590 <https://github.com/coq/coq/pull/11590>`_,
-  by Hugo Herbelin, fixes `#9741 <https://github.com/coq/coq/pull/9741>`_).
diff --git a/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst b/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst
deleted file mode 100644
index 1d30d16664..0000000000
--- a/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Added:**
-  Notations declared with the ``where`` clause in the declaration of
-  inductive types, coinductive types, record fields, fixpoints and
-  cofixpoints now support the ``only parsing`` modifier
-  (`#11602 <https://github.com/coq/coq/pull/11602>`_,
-  by Hugo Herbelin).
diff --git a/doc/changelog/03-notations/11650-parensNew.rst b/doc/changelog/03-notations/11650-parensNew.rst
deleted file mode 100644
index f52a720428..0000000000
--- a/doc/changelog/03-notations/11650-parensNew.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  added the :flag:`Printing Parentheses` flag to print parentheses even when implied by associativity or precedence.
-  (`#11650 <https://github.com/coq/coq/pull/11650>`_,
-  by Hugo Herbelin and Abhishek Anand).
diff --git a/doc/changelog/03-notations/11848-nicer-decimal-printing.rst b/doc/changelog/03-notations/11848-nicer-decimal-printing.rst
deleted file mode 100644
index 1d3a390f36..0000000000
--- a/doc/changelog/03-notations/11848-nicer-decimal-printing.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Changed:**
-  Nicer printing for decimal constants in R and Q.
-  1.5 is now printed 1.5 rather than 15e-1.
-  (`#11848 <https://github.com/coq/coq/pull/11848>`_,
-  by Pierre Roux).
diff --git a/doc/changelog/03-notations/11948-hexadecimal.rst b/doc/changelog/03-notations/11948-hexadecimal.rst
deleted file mode 100644
index e4b76d238c..0000000000
--- a/doc/changelog/03-notations/11948-hexadecimal.rst
+++ /dev/null
@@ -1,12 +0,0 @@
-- **Added:**
-  Numeral notations now parse hexadecimal constants such as ``0x2a``
-  or ``0xb.2ap-2``. Parsers added for :g:`nat`, :g:`positive`, :g:`Z`,
-  :g:`N`, :g:`Q`, :g:`R`, primitive integers and primitive floats
-  (`#11948 <https://github.com/coq/coq/pull/11948>`_,
-  by Pierre Roux).
-- **Deprecated:**
-  Numeral Notation on ``Decimal.uint``, ``Decimal.int`` and
-  ``Decimal.decimal`` are replaced respectively by numeral notations
-  on ``Numeral.uint``, ``Numeral.int`` and ``Numeral.numeral``
-  (`#11948 <https://github.com/coq/coq/pull/11948>`_,
-  by Pierre Roux).
diff --git a/doc/changelog/03-notations/12163-fix-12159.rst b/doc/changelog/03-notations/12163-fix-12159.rst
deleted file mode 100644
index 978ed561dd..0000000000
--- a/doc/changelog/03-notations/12163-fix-12159.rst
+++ /dev/null
@@ -1,11 +0,0 @@
-- **Fixed:**
-  Numeral Notations now play better with multiple scopes for the same
-  inductive type. Previously, when multiple numeral notations were defined
-  for the same inductive, only the last one was considered for
-  printing. Now, among the notations that are usable for printing and either
-  have a scope delimiter or are open, the selection is made according
-  to the order of open scopes, or according to the last defined
-  notation if no appropriate scope is open
-  (`#12163 <https://github.com/coq/coq/pull/12163>`_,
-  fixes `#12159 <https://github.com/coq/coq/pull/12159>`_,
-  by Pierre Roux, review by Hugo Herbelin and Jason Gross).
diff --git a/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst b/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst
deleted file mode 100644
index e1fcfb78c4..0000000000
--- a/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  Abbreviations support arguments occurring both in term and binder position
-  (`#8808 <https://github.com/coq/coq/pull/8808>`_,
-  by Hugo Herbelin).