From e9b3040326632589d811253e91de4f27c9cf70b4 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 1 Dec 2020 15:05:35 +0100
Subject: Changes without PR references fixes

---
 doc/sphinx/changes.rst | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 0626f240fd..c9968a64b2 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -292,15 +292,21 @@ Notations
   by Hugo Herbelin).
 - **Deprecated**
   ``Numeral.v`` is deprecated, please use ``Number.v`` instead.
+  (`#12218 <https://github.com/coq/coq/pull/12218>`_,
+  by Pierre Roux).
 - **Changed**
   Rational and real constants are parsed differently.
   The exponent is now encoded separately from the fractional part
   using ``Z.pow_pos``. This way, parsing large exponents can no longer
   blow up and constants are printed in a form closer to the one in which they
   were parsed (i.e., ``102e-2`` is reprinted as such and not ``1.02``).
+  (`#12218 <https://github.com/coq/coq/pull/12218>`_,
+  by Pierre Roux).
 - **Removed**
   OCaml parser and printer for real constants have been removed.
   Real constants are now handled with proven Coq code.
+  (`#12218 <https://github.com/coq/coq/pull/12218>`_,
+  by Pierre Roux).
 - **Added:**
   :ref:`Number Notation <number-notations>` and :ref:`String Notation
   <string-notations>` commands now
@@ -543,8 +549,8 @@ Commands and options
   by Pierre-Marie Pédrot).
 - **Changed:**
   The :attr:`export` locality can now be used for all Hint commands,
-  including :tacn:`Hint Cut`, :tacn:`Hint Mode`, :tacn:`Hint Transparent` / `Opaque` and
-  :tacn:`Remove Hints`
+  including :cmd:`Hint Cut`, :cmd:`Hint Mode`, :cmd:`Hint Transparent` / `Opaque` and
+  :cmd:`Remove Hints`
   (`#13388 <https://github.com/coq/coq/pull/13388>`_,
   by Pierre-Marie Pédrot).
 
-- 
cgit v1.2.3