From c02bbaeb9c6c9cbc4a7f2dc47876a94fdd33aa5e Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 9 Feb 2021 18:23:11 +0100
Subject: Remove decimal-only number notations

This was deprecated in 8.12
---
 doc/sphinx/user-extensions/syntax-extensions.rst | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 03571ad680..557ef10555 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1726,12 +1726,6 @@ Number notations
             * :n:`@qualid__type -> Number.number`
             * :n:`@qualid__type -> option Number.number`
 
-         .. deprecated:: 8.12
-            Number notations on :g:`Decimal.uint`, :g:`Decimal.int` and
-            :g:`Decimal.decimal` are replaced respectively by number
-            notations on :g:`Number.uint`, :g:`Number.int` and
-            :g:`Number.number`.
-
          When parsing, the application of the parsing function
          :n:`@qualid__parse` to the number will be fully reduced, and universes
          of the resulting term will be refreshed.
-- 
cgit v1.2.3