Merge PR #12979: Uniformize names for number literals between parsing and refman

Reviewed-by: herbelin
Reviewed-by: jfehrle
Ack-by: Zimmi48
Ack-by: proux01

8 files changed, 30 insertions, 17 deletions

diff --git a/plugins/cc/g_congruence.mlg b/plugins/cc/g_congruence.mlg
index 3920e3da75..2c91901477 100644
--- a/plugins/cc/g_congruence.mlg
+++ b/plugins/cc/g_congruence.mlg
@@ -22,9 +22,9 @@ DECLARE PLUGIN "cc_plugin"
 
 TACTIC EXTEND cc
 | [ "congruence" ] -> { congruence_tac 1000 [] }
-| [ "congruence" integer(n) ] -> { congruence_tac n [] }
+| [ "congruence" natural(n) ] -> { congruence_tac n [] }
 | [ "congruence" "with" ne_constr_list(l) ] -> { congruence_tac 1000 l }
- |[ "congruence" integer(n) "with" ne_constr_list(l) ] ->
+| [ "congruence" natural(n) "with" ne_constr_list(l) ] ->
    { congruence_tac n l }
 END
 
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 35c90444b1..8d197e6056 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -77,7 +77,7 @@ END
 (* true = All transparent, false = Opaque if possible *)
 
 VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> {
+ | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> {
      set_typeclasses_debug d;
      Option.iter set_typeclasses_strategy s;
      set_typeclasses_depth depth
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 114acaa412..78cde2cde8 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -271,7 +271,7 @@ GRAMMAR EXTEND Gram
   message_token:
     [ [ id = identref -> { MsgIdent id }
       | s = STRING -> { MsgString s }
-      | n = integer -> { MsgInt n } ] ]
+      | n = natural -> { MsgInt n } ] ]
   ;
 
   ltac_def_kind:
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index fa176482bf..a6673699af 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -88,13 +88,13 @@ let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
 }
 
 VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_program
-| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
+| [ "Obligation" natural(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
     { obligation (num, Some name, Some t) tac }
-| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
+| [ "Obligation" natural(num) "of" ident(name) withtac(tac) ] ->
     { obligation (num, Some name, None) tac }
-| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
+| [ "Obligation" natural(num) ":" lglob(t) withtac(tac) ] ->
     { obligation (num, None, Some t) tac }
-| [ "Obligation" integer(num) withtac(tac) ] ->
+| [ "Obligation" natural(num) withtac(tac) ] ->
     { obligation (num, None, None) tac }
 | [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
     { next_obligation (Some name) tac }
@@ -102,9 +102,9 @@ VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_
 END
 
 VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF STATE program
-| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] ->
+| [ "Solve" "Obligation" natural(num) "of" ident(name) "with" tactic(t) ] ->
     { try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) }
-| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] ->
+| [ "Solve" "Obligation" natural(num) "with" tactic(t) ] ->
     { try_solve_obligation num None (Some (Tacinterp.interp t)) }
 END
 
diff --git a/plugins/ltac/profile_ltac_tactics.mlg b/plugins/ltac/profile_ltac_tactics.mlg
index eb9d9cbdce..e5309ea441 100644
--- a/plugins/ltac/profile_ltac_tactics.mlg
+++ b/plugins/ltac/profile_ltac_tactics.mlg
@@ -55,7 +55,7 @@ END
 
 TACTIC EXTEND show_ltac_profile
 | [ "show" "ltac" "profile" ] -> { tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff }
-| [ "show" "ltac" "profile" "cutoff" int(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) }
+| [ "show" "ltac" "profile" "cutoff" integer(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) }
 | [ "show" "ltac" "profile" string(s) ] -> { tclSHOW_PROFILE_TACTIC s }
 END
 
@@ -74,7 +74,7 @@ END
 
 VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
 | [ "Show" "Ltac" "Profile" ] -> { print_results ~cutoff:!Flags.profile_ltac_cutoff }
-| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> { print_results ~cutoff:(float_of_int n) }
+| [ "Show" "Ltac" "Profile" "CutOff" integer(n) ] -> { print_results ~cutoff:(float_of_int n) }
 END
 
 VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 88480194c8..2258201c22 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2028,6 +2028,9 @@ let () =
   declare_uniform wit_int
 
 let () =
+  declare_uniform wit_nat
+
+let () =
   declare_uniform wit_bool
 
 let () =
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 60af804c1b..98439e27a1 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -219,20 +219,20 @@ let test_ssrslashnum b1 b2 _ strm =
   match Util.stream_nth 0 strm with
   | Tok.KEYWORD "/" ->
       (match Util.stream_nth 1 strm with
-      | Tok.NUMERAL _ when b1 ->
+      | Tok.NUMBER _ when b1 ->
          (match Util.stream_nth 2 strm with
          | Tok.KEYWORD "=" | Tok.KEYWORD "/=" when not b2 -> ()
          | Tok.KEYWORD "/" ->
              if not b2 then () else begin
                match Util.stream_nth 3 strm with
-               | Tok.NUMERAL _ -> ()
+               | Tok.NUMBER _ -> ()
                | _ -> raise Stream.Failure
              end
          | _ -> raise Stream.Failure)
       | Tok.KEYWORD "/" when not b1 ->
          (match Util.stream_nth 2 strm with
          | Tok.KEYWORD "=" when not b2 -> ()
-         | Tok.NUMERAL _ when b2 ->
+         | Tok.NUMBER _ when b2 ->
            (match Util.stream_nth 3 strm with
            | Tok.KEYWORD "=" -> ()
            | _ -> raise Stream.Failure)
@@ -243,7 +243,7 @@ let test_ssrslashnum b1 b2 _ strm =
   | Tok.KEYWORD "//" when not b1 ->
          (match Util.stream_nth 1 strm with
          | Tok.KEYWORD "=" when not b2 -> ()
-         | Tok.NUMERAL _ when b2 ->
+         | Tok.NUMBER _ when b2 ->
            (match Util.stream_nth 2 strm with
            | Tok.KEYWORD "=" -> ()
            | _ -> raise Stream.Failure)
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index e66dbe17b2..c030925ea9 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -24,6 +24,11 @@ let pr_numnot_option = function
   | Warning n -> str "(warning after " ++ NumTok.UnsignedNat.print n ++ str ")"
   | Abstract n -> str "(abstract after " ++ NumTok.UnsignedNat.print n ++ str ")"
 
+let warn_deprecated_numeral_notation =
+  CWarnings.create ~name:"numeral-notation" ~category:"deprecated"
+    (fun () ->
+      strbrk "Numeral Notation is deprecated, please use Number Notation instead.")
+
 }
 
 VERNAC ARGUMENT EXTEND numnotoption
@@ -34,8 +39,13 @@ VERNAC ARGUMENT EXTEND numnotoption
 END
 
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
-  | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
+  | #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) ":"
       ident(sc) numnotoption(o) ] ->
 
     { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
+  | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
+      ident(sc) numnotoption(o) ] ->
+
+    { warn_deprecated_numeral_notation ();
+      vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
 END