Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12)

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

6 files changed, 5 insertions, 72 deletions

diff --git a/dev/ci/user-overlays/13842-proux01-remove-decimal.sh b/dev/ci/user-overlays/13842-proux01-remove-decimal.sh
new file mode 100644
index 0000000000..5ede8221ce
--- /dev/null
+++ b/dev/ci/user-overlays/13842-proux01-remove-decimal.sh
@@ -0,0 +1 @@
+overlay hott https://github.com/proux01/HoTT coq-13842 13842
diff --git a/doc/changelog/03-notations/13842-remove-decimal.rst b/doc/changelog/03-notations/13842-remove-decimal.rst
new file mode 100644
index 0000000000..4bc26ef6a8
--- /dev/null
+++ b/doc/changelog/03-notations/13842-remove-decimal.rst
@@ -0,0 +1,3 @@
+- **Removed:**
+  Remove decimal-only number notations which were deprecated in 8.12.
+  (`#13842 <https://github.com/coq/coq/pull/13842>`_, by Pierre Roux).
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.
diff --git a/interp/notation.ml b/interp/notation.ml
index ed605c994d..4010c3487e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -557,9 +557,6 @@ type target_kind =
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
   | Int63 of pos_neg_int63_ty (* Coq.Numbers.Cyclic.Int63.PrimInt63.pos_neg_int63 *)
   | Number of number_ty (* Coq.Init.Number.number + uint + int *)
-  | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *)
-  | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *)
-  | Decimal of number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
 
 type string_target_kind =
   | ListByte
@@ -872,30 +869,16 @@ let mkDecHex ind c n = match c with
   | CDec -> mkApp (mkConstruct (ind, 1), [|n|])  (* (UInt|Int|)Decimal *)
   | CHex -> mkApp (mkConstruct (ind, 2), [|n|])  (* (UInt|Int|)Hexadecimal *)
 
-exception NonDecimal
-
-let decimal_coqnumber_of_rawnum inds n =
-  if NumTok.Signed.classify n <> CDec then raise NonDecimal;
-  coqnumber_of_rawnum inds CDec n
-
 let coqnumber_of_rawnum inds n =
   let c = NumTok.Signed.classify n in
   let n = coqnumber_of_rawnum inds c n in
   mkDecHex inds.number c n
 
-let decimal_coquint_of_rawnum inds n =
-  if NumTok.UnsignedNat.classify n <> CDec then raise NonDecimal;
-  coquint_of_rawnum inds CDec (Some n)
-
 let coquint_of_rawnum inds n =
   let c = NumTok.UnsignedNat.classify n in
   let n = coquint_of_rawnum inds c (Some n) in
   mkDecHex inds.uint c n
 
-let decimal_coqint_of_rawnum inds n =
-  if NumTok.SignedNat.classify n <> CDec then raise NonDecimal;
-  coqint_of_rawnum inds CDec n
-
 let coqint_of_rawnum inds n =
   let c = NumTok.SignedNat.classify n in
   let n = coqint_of_rawnum inds c n in
@@ -950,23 +933,14 @@ let destDecHex c = match Constr.kind c with
       | _ -> raise NotAValidPrimToken)
   | _ -> raise NotAValidPrimToken
 
-let decimal_rawnum_of_coqnumber c =
-  rawnum_of_coqnumber CDec c
-
 let rawnum_of_coqnumber c =
   let cl, c = destDecHex c in
   rawnum_of_coqnumber cl c
 
-let decimal_rawnum_of_coquint c =
-  rawnum_of_coquint CDec c
-
 let rawnum_of_coquint c =
   let cl, c = destDecHex c in
   rawnum_of_coquint cl c
 
-let decimal_rawnum_of_coqint c =
-  rawnum_of_coqint CDec c
-
 let rawnum_of_coqint c =
   let cl, c = destDecHex c in
   rawnum_of_coqint cl c
@@ -1084,22 +1058,13 @@ let interp o ?loc n =
        coqint_of_rawnum int_ty n
     | UInt int_ty, Some (SPlus, n) ->
        coquint_of_rawnum int_ty n
-    | DecimalInt int_ty, Some n ->
-       (try decimal_coqint_of_rawnum int_ty n
-        with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
-    | DecimalUInt int_ty, Some (SPlus, n) ->
-       (try decimal_coquint_of_rawnum int_ty n
-        with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
     | Z z_pos_ty, Some n ->
        z_of_bigint z_pos_ty (NumTok.SignedNat.to_bigint n)
     | Int63 pos_neg_int63_ty, Some n ->
        interp_int63 ?loc pos_neg_int63_ty.pos_neg_int63_ty (NumTok.SignedNat.to_bigint n)
-    | (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63 _), _ ->
+    | (Int _ | UInt _ | Z _ | Int63 _), _ ->
        no_such_prim_token "number" ?loc o.ty_name
     | Number number_ty, _ -> coqnumber_of_rawnum number_ty n
-    | Decimal number_ty, _ ->
-       (try decimal_coqnumber_of_rawnum number_ty n
-        with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
   in
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -1124,9 +1089,6 @@ let uninterp o n =
       | (Z _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_z c)
       | (Int63 _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_coqpos_neg_int63 c)
       | (Number _, c) -> rawnum_of_coqnumber c
-      | (DecimalInt _, c) -> NumTok.Signed.of_int (decimal_rawnum_of_coqint c)
-      | (DecimalUInt _, c) -> NumTok.Signed.of_nat (decimal_rawnum_of_coquint c)
-      | (Decimal _, c) -> decimal_rawnum_of_coqnumber c
     end o n
 end
 
diff --git a/interp/notation.mli b/interp/notation.mli
index 77f245ae77..195f2a4416 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -146,9 +146,6 @@ type target_kind =
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
   | Int63 of pos_neg_int63_ty (* Coq.Numbers.Cyclic.Int63.PrimInt63.pos_neg_int63 *)
   | Number of number_ty (* Coq.Init.Number.number + uint + int *)
-  | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *)
-  | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *)
-  | Decimal of number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
 
 type string_target_kind =
   | ListByte
diff --git a/plugins/syntax/number.ml b/plugins/syntax/number.ml
index 80c11dc0d4..551e2bac5d 100644
--- a/plugins/syntax/number.ml
+++ b/plugins/syntax/number.ml
@@ -131,13 +131,6 @@ let type_error_of g ty =
      str " to Number.int or (option Number.int)." ++ fnl () ++
      str "Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or Number.number could be used (you may need to require BinNums or Number or PrimInt63 first).")
 
-let warn_deprecated_decimal =
-  CWarnings.create ~name:"decimal-numeral-notation" ~category:"deprecated"
-    (fun () ->
-      strbrk "Deprecated Number Notation for Decimal.uint, \
-              Decimal.int or Decimal.decimal. Use Number.uint, \
-              Number.int or Number.number respectively.")
-
 let error_params ind =
   CErrors.user_err
     (str "Wrong number of parameters for inductive" ++ spc ()
@@ -456,12 +449,6 @@ let vernac_number_notation local ty f g opts scope =
     | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty, Option
     | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Number num_ty, Direct
     | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Number num_ty, Option
-    | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint cty) -> DecimalInt int_ty, Direct
-    | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> DecimalInt int_ty, Option
-    | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint cty) -> DecimalUInt int_ty, Direct
-    | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> DecimalUInt int_ty, Option
-    | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec cty) -> Decimal num_ty, Direct
-    | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec (opt cty)) -> Decimal num_ty, Option
     | _ ->
     match z_pos_ty with
     | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct
@@ -484,12 +471,6 @@ let vernac_number_notation local ty f g opts scope =
     | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty, Option
     | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Number num_ty, Direct
     | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Number num_ty, Option
-    | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty cint) -> DecimalInt int_ty, Direct
-    | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> DecimalInt int_ty, Option
-    | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty cuint) -> DecimalUInt int_ty, Direct
-    | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> DecimalUInt int_ty, Option
-    | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty cdec) -> Decimal num_ty, Direct
-    | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty (opt cdec)) -> Decimal num_ty, Option
     | _ ->
     match z_pos_ty with
     | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct
@@ -500,11 +481,6 @@ let vernac_number_notation local ty f g opts scope =
     | Some (pos_neg_int63_ty, cint63) when has_type env sigma g (arrow cty (opt cint63)) -> Int63 pos_neg_int63_ty, Option
     | _ -> type_error_of g ty
   in
-  (match to_kind, of_kind with
-   | ((DecimalInt _ | DecimalUInt _ | Decimal _), _), _
-   | _, ((DecimalInt _ | DecimalUInt _ | Decimal _), _) ->
-      warn_deprecated_decimal ()
-   | _ -> ());
   let to_post, pt_required, pt_refs = match tyc_params with
     | TargetPrim path -> [||], path, [Coqlib.lib_ref "num.int63.wrap_int"]
     | TargetInd (tyc, params) ->