[refman] Rename num to natural

2 files changed, 67 insertions, 72 deletions

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 549ace5d13..ff40555696 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -749,7 +749,7 @@ digit: [
 | "0" ".." "9"
 ]
 
-decnum: [
+decnat: [
 | digit LIST0 [ digit | "_" ]
 ]
 
@@ -757,26 +757,22 @@ hexdigit: [
 | [ "0" ".." "9" | "a" ".." "f" | "A" ".." "F" ]
 ]
 
-hexnum: [
+hexnat: [
 | [ "0x" | "0X" ] hexdigit LIST0 [ hexdigit | "_" ]
 ]
 
-num: [
-| [ decnum | hexnum ]
-]
-
-natural: [ | DELETENT ]
 natural: [
-| num  (* todo: or should it be "nat"? *)
+| REPLACE bignat
+| WITH [ decnat | hexnat ]
 ]
 
 int: [
-| OPT "-" num
+| OPT "-" natural
 ]
 
 numeral: [
-| OPT "-" decnum OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnum )
-| OPT "-" hexnum OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnum )
+| OPT "-" decnat OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnat )
+| OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat )
 ]
 
 bigint: [
@@ -1841,7 +1837,7 @@ query_command: [ ] (* re-add as a placeholder *)
 
 sentence: [
 | OPT attributes command "."
-| OPT attributes OPT ( num ":" ) query_command "."
+| OPT attributes OPT ( natural ":" ) query_command "."
 | OPT attributes OPT ( toplevel_selector ":" ) tactic_expr5 [ "." | "..." ]
 | control_command
 ]
@@ -2053,8 +2049,8 @@ tac2rec_fields: [
 
 (* todo: weird productions, ints only after an initial "-"??:
   occs_nums: [
-  | LIST1 [ num | ident ]
-  | "-" [ num | ident ] LIST0 int_or_var
+  | LIST1 [ natural | ident ]
+  | "-" [ natural | ident ] LIST0 int_or_var
 *)
 ltac2_occs_nums: [
 | DELETE LIST1 nat_or_anti      (* Ltac2 plugin *)
@@ -2160,7 +2156,7 @@ RENAME: [
 | Prim.string string
 | Prim.integer int
 | Prim.qualid qualid
-| Prim.natural num
+| Prim.natural natural
 ]
 
 gmatch_list: [
@@ -2210,7 +2206,6 @@ SPLICE: [
 | match_context_list
 | IDENT
 | LEFTQMARK
-| natural
 | NUMBER
 | STRING
 | hyp
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 3cd5a85654..6d07f6b0c4 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -130,19 +130,19 @@ type: [
 ]
 
 numeral: [
-| OPT "-" decnum OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnum )
-| OPT "-" hexnum OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnum )
+| OPT "-" decnat OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnat )
+| OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat )
 ]
 
 int: [
-| OPT "-" num
+| OPT "-" natural
 ]
 
-num: [
-| [ decnum | hexnum ]
+natural: [
+| [ decnat | hexnat ]
 ]
 
-decnum: [
+decnat: [
 | digit LIST0 [ digit | "_" ]
 ]
 
@@ -150,7 +150,7 @@ digit: [
 | "0" ".." "9"
 ]
 
-hexnum: [
+hexnat: [
 | [ "0x" | "0X" ] hexdigit LIST0 [ hexdigit | "_" ]
 ]
 
@@ -230,7 +230,7 @@ nonterminal: [
 
 sentence: [
 | OPT attributes command "."
-| OPT attributes OPT ( num ":" ) query_command "."
+| OPT attributes OPT ( natural ":" ) query_command "."
 | OPT attributes OPT ( toplevel_selector ":" ) ltac_expr [ "." | "..." ]
 | control_command
 ]
@@ -277,7 +277,7 @@ universe: [
 ]
 
 universe_expr: [
-| universe_name OPT ( "+" num )
+| universe_name OPT ( "+" natural )
 ]
 
 universe_name: [
@@ -509,8 +509,8 @@ ref_or_pattern_occ: [
 ]
 
 occs_nums: [
-| LIST1 [ num | ident ]
-| "-" [ num | ident ] LIST0 int_or_var
+| LIST1 [ natural | ident ]
+| "-" [ natural | ident ] LIST0 int_or_var
 ]
 
 int_or_var: [
@@ -535,7 +535,7 @@ record_definition: [
 ]
 
 record_field: [
-| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) name OPT field_body OPT [ "|" num ] OPT decl_notations
+| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) name OPT field_body OPT [ "|" natural ] OPT decl_notations
 ]
 
 field_body: [
@@ -589,7 +589,7 @@ sort_family: [
 ]
 
 hint_info: [
-| "|" OPT num OPT one_term
+| "|" OPT natural OPT one_term
 ]
 
 module_binder: [
@@ -602,7 +602,7 @@ module_type_inl: [
 ]
 
 functor_app_annot: [
-| "[" "inline" "at" "level" num "]"
+| "[" "inline" "at" "level" natural "]"
 | "[" "no" "inline" "]"
 ]
 
@@ -714,7 +714,7 @@ command: [
 | "Locate" reference
 | "Locate" "Term" reference
 | "Locate" "Module" qualid
-| "Info" num ltac_expr
+| "Info" natural ltac_expr
 | "Locate" "Ltac" qualid
 | "Locate" "Library" qualid
 | "Locate" "File" string
@@ -762,7 +762,7 @@ command: [
 | "Print" "Module" "Type" qualid
 | "Print" "Module" qualid
 | "Print" "Namespace" dirpath
-| "Inspect" num
+| "Inspect" natural
 | "Add" "ML" "Path" string
 | OPT "Export" "Set" setting_name
 | "Print" "Table" setting_name
@@ -773,7 +773,7 @@ command: [
 | "Restore" "State" [ ident | string ]
 | "Reset" "Initial"
 | "Reset" ident
-| "Back" OPT num
+| "Back" OPT natural
 | "Debug" [ "On" | "Off" ]
 | "Declare" "Reduction" ident ":=" red_expr
 | "Declare" "Custom" "Entry" ident
@@ -802,17 +802,17 @@ command: [
 | "Proof" "Mode" string
 | "Proof" term
 | "Abort" OPT [ "All" | ident ]
-| "Existential" num OPT ( ":" term ) ":=" term
+| "Existential" natural OPT ( ":" term ) ":=" term
 | "Admitted"
 | "Qed"
 | "Save" ident
 | "Defined" OPT ident
 | "Restart"
-| "Undo" OPT ( OPT "To" num )
-| "Focus" OPT num
+| "Undo" OPT ( OPT "To" natural )
+| "Focus" OPT natural
 | "Unfocus"
 | "Unfocused"
-| "Show" OPT [ ident | num ]
+| "Show" OPT [ ident | natural ]
 | "Show" "Existentials"
 | "Show" "Universes"
 | "Show" "Conjectures"
@@ -824,7 +824,7 @@ command: [
 | "Create" "HintDb" ident OPT "discriminated"
 | "Remove" "Hints" LIST1 qualid OPT ( ":" LIST1 ident )
 | "Hint" hint OPT ( ":" LIST1 ident )
-| "Comments" LIST0 [ one_term | string | num ]
+| "Comments" LIST0 [ one_term | string | natural ]
 | "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info
 | "Declare" "Scope" scope_name
 | "Obligation" int OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) )
@@ -894,7 +894,7 @@ command: [
 | "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" eauto_search_strategy_name ")" ) OPT int
 | "Proof" "with" ltac_expr OPT [ "using" section_subset_expr ]
 | "Proof" "using" section_subset_expr OPT [ "with" ltac_expr ]
-| "Tactic" "Notation" OPT ( "(" "at" "level" num ")" ) LIST1 ltac_production_item ":=" ltac_expr
+| "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr
 | "Print" "Rewrite" "HintDb" ident
 | "Print" "Ltac" qualid
 | "Ltac" tacdef_body LIST0 ( "with" tacdef_body )
@@ -916,7 +916,7 @@ command: [
 | "String" "Notation" qualid qualid qualid ":" scope_name
 | "SubClass" ident_decl def_body
 | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ]
-| assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ]
+| assumption_token OPT ( "Inline" OPT ( "(" natural ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ]
 | [ "Definition" | "Example" ] ident_decl def_body
 | "Let" ident_decl def_body
 | "Inductive" inductive_definition LIST0 ( "with" inductive_definition )
@@ -959,7 +959,7 @@ command: [
 | "Context" LIST1 binder
 | "Instance" OPT ( ident_decl LIST0 binder ) ":" term OPT hint_info OPT [ ":=" "{" LIST0 field_def "}" | ":=" term ]
 | "Existing" "Instance" qualid OPT hint_info
-| "Existing" "Instances" LIST1 qualid OPT [ "|" num ]
+| "Existing" "Instances" LIST1 qualid OPT [ "|" natural ]
 | "Existing" "Class" qualid
 | "Arguments" reference LIST0 arg_specs LIST0 [ "," LIST0 implicits_alt ] OPT [ ":" LIST1 args_modifier SEP "," ]
 | "Implicit" [ "Type" | "Types" ] reserv_list
@@ -995,12 +995,12 @@ command: [
 | "Print" "Ltac2" qualid      (* Ltac2 plugin *)
 | "Time" sentence
 | "Redirect" string sentence
-| "Timeout" num sentence
+| "Timeout" natural sentence
 | "Fail" sentence
 | "Drop"
 | "Quit"
-| "BackTo" num
-| "Show" "Goal" num "at" num
+| "BackTo" natural
+| "Show" "Goal" natural "at" natural
 ]
 
 section_subset_expr: [
@@ -1067,8 +1067,8 @@ univ_name_list: [
 
 hint: [
 | "Resolve" LIST1 [ qualid | one_term ] OPT hint_info
-| "Resolve" "->" LIST1 qualid OPT num
-| "Resolve" "<-" LIST1 qualid OPT num
+| "Resolve" "->" LIST1 qualid OPT natural
+| "Resolve" "<-" LIST1 qualid OPT natural
 | "Immediate" LIST1 [ qualid | one_term ]
 | "Variables" "Transparent"
 | "Variables" "Opaque"
@@ -1079,7 +1079,7 @@ hint: [
 | "Mode" qualid LIST1 [ "+" | "!" | "-" ]
 | "Unfold" LIST1 qualid
 | "Constructors" LIST1 qualid
-| "Extern" num OPT one_term "=>" ltac_expr
+| "Extern" natural OPT one_term "=>" ltac_expr
 ]
 
 tacdef_body: [
@@ -1127,7 +1127,7 @@ lident: [
 ]
 
 destruction_arg: [
-| num
+| natural
 | constr_with_bindings
 | constr_with_bindings_arg
 ]
@@ -1221,7 +1221,7 @@ q_destruction_arg: [
 ]
 
 ltac2_destruction_arg: [
-| num      (* Ltac2 plugin *)
+| natural      (* Ltac2 plugin *)
 | lident      (* Ltac2 plugin *)
 | ltac2_constr_with_bindings      (* Ltac2 plugin *)
 ]
@@ -1249,7 +1249,7 @@ ltac2_simple_binding: [
 
 qhyp: [
 | "$" ident      (* Ltac2 plugin *)
-| num      (* Ltac2 plugin *)
+| natural      (* Ltac2 plugin *)
 | lident      (* Ltac2 plugin *)
 ]
 
@@ -1318,8 +1318,8 @@ class: [
 ]
 
 syntax_modifier: [
-| "at" "level" num
-| "in" "custom" ident OPT ( "at" "level" num )
+| "at" "level" natural
+| "in" "custom" ident OPT ( "at" "level" natural )
 | LIST1 ident SEP "," "at" level
 | ident "at" level OPT binder_interp
 | ident explicit_subentry
@@ -1336,12 +1336,12 @@ explicit_subentry: [
 | "ident"
 | "global"
 | "bigint"
-| "strict" "pattern" OPT ( "at" "level" num )
+| "strict" "pattern" OPT ( "at" "level" natural )
 | "binder"
 | "closed" "binder"
 | "constr" OPT ( "at" level ) OPT binder_interp
 | "custom" ident OPT ( "at" level ) OPT binder_interp
-| "pattern" OPT ( "at" "level" num )
+| "pattern" OPT ( "at" "level" natural )
 ]
 
 binder_interp: [
@@ -1351,7 +1351,7 @@ binder_interp: [
 ]
 
 level: [
-| "level" num
+| "level" natural
 | "next" "level"
 ]
 
@@ -1388,14 +1388,14 @@ simple_tactic: [
 | "esplit" OPT ( "with" bindings )
 | "exists" OPT ( LIST1 bindings SEP "," )
 | "eexists" OPT ( LIST1 bindings SEP "," )
-| "intros" "until" [ ident | num ]
+| "intros" "until" [ ident | natural ]
 | "intro" OPT ident OPT where
 | "move" ident OPT where
 | "rename" LIST1 ( ident "into" ident ) SEP ","
 | "revert" LIST1 ident
-| "simple" "induction" [ ident | num ]
-| "simple" "destruct" [ ident | num ]
-| "double" "induction" [ ident | num ] [ ident | num ]
+| "simple" "induction" [ ident | natural ]
+| "simple" "destruct" [ ident | natural ]
+| "double" "induction" [ ident | natural ] [ ident | natural ]
 | "admit"
 | "clear" LIST0 ident
 | "clear" "-" LIST1 ident
@@ -1551,7 +1551,7 @@ simple_tactic: [
 | "eelim" constr_with_bindings_arg OPT ( "using" constr_with_bindings )
 | "case" induction_clause_list
 | "ecase" induction_clause_list
-| "fix" ident num OPT ( "with" LIST1 fixdecl )
+| "fix" ident natural OPT ( "with" LIST1 fixdecl )
 | "cofix" ident OPT ( "with" LIST1 cofixdecl )
 | "pose" bindings_with_parameters
 | "pose" one_term OPT as_name
@@ -1585,11 +1585,11 @@ simple_tactic: [
 | "edestruct" induction_clause_list
 | "rewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 )
 | "erewrite" LIST1 oriented_rewriter SEP "," OPT clause_dft_concl OPT ( "by" ltac_expr3 )
-| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] [ ident | num ] OPT as_or_and_ipat OPT [ "with" one_term ]
-| "simple" "inversion" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
-| "inversion" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
-| "inversion_clear" [ ident | num ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
-| "inversion" [ ident | num ] "using" one_term OPT ( "in" LIST1 ident )
+| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] [ ident | natural ] OPT as_or_and_ipat OPT [ "with" one_term ]
+| "simple" "inversion" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
+| "inversion" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
+| "inversion_clear" [ ident | natural ] OPT as_or_and_ipat OPT ( "in" LIST1 ident )
+| "inversion" [ ident | natural ] "using" one_term OPT ( "in" LIST1 ident )
 | "red" OPT clause_dft_concl
 | "hnf" OPT clause_dft_concl
 | "simpl" OPT delta_flag OPT ref_or_pattern_occ OPT clause_dft_concl
@@ -1610,7 +1610,7 @@ simple_tactic: [
 | "f_equal"
 | "firstorder" OPT ltac_expr firstorder_rhs
 | "gintuition" OPT ltac_expr
-| "functional" "inversion" [ ident | num ] OPT qualid      (* funind plugin *)
+| "functional" "inversion" [ ident | natural ] OPT qualid      (* funind plugin *)
 | "functional" "induction" term OPT fun_ind_using OPT with_names      (* funind plugin *)
 | "soft" "functional" "induction" LIST1 one_term OPT fun_ind_using OPT with_names      (* funind plugin *)
 | "psatz_Z" OPT int_or_var ltac_expr
@@ -1698,7 +1698,7 @@ as_name: [
 ]
 
 rewriter: [
-| OPT num OPT [ "?" | "!" ] constr_with_bindings_arg
+| OPT natural OPT [ "?" | "!" ] constr_with_bindings_arg
 ]
 
 oriented_rewriter: [
@@ -1758,7 +1758,7 @@ simple_intropattern_closed: [
 
 simple_binding: [
 | "(" ident ":=" term ")"
-| "(" num ":=" term ")"
+| "(" natural ":=" term ")"
 ]
 
 bindings: [
@@ -1807,7 +1807,7 @@ ltac2_occs: [
 ]
 
 ltac2_occs_nums: [
-| OPT "-" LIST1 [ num      (* Ltac2 plugin *) | "$" ident ]      (* Ltac2 plugin *)
+| OPT "-" LIST1 [ natural      (* Ltac2 plugin *) | "$" ident ]      (* Ltac2 plugin *)
 ]
 
 ltac2_concl_occ: [
@@ -1858,7 +1858,7 @@ ltac2_oriented_rewriter: [
 ]
 
 ltac2_rewriter: [
-| OPT num OPT [ "?" | "!" ] ltac2_constr_with_bindings
+| OPT natural OPT [ "?" | "!" ] ltac2_constr_with_bindings
 ]
 
 q_dispatch: [
@@ -2328,8 +2328,8 @@ selector: [
 ]
 
 range_selector: [
-| num "-" num
-| num
+| natural "-" natural
+| natural
 ]
 
 match_key: [