From b4d11894fd676ec53e4fdf860d32173a778242c5 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 4 Sep 2020 15:02:00 +0200
Subject: [parsing] Rename token NUMERAL to NUMBER

---
 doc/tools/docgram/common.edit_mlg |  8 ++++----
 doc/tools/docgram/fullGrammar     | 10 +++++-----
 2 files changed, 9 insertions(+), 9 deletions(-)

(limited to 'doc/tools')

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 9971a03894..a619089cdd 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -300,7 +300,7 @@ term_let: [
 
 atomic_constr: [
 | MOVETO qualid_annotated global univ_instance
-| MOVETO primitive_notations NUMERAL
+| MOVETO primitive_notations NUMBER
 | MOVETO primitive_notations string
 | MOVETO term_evar "_"
 | REPLACE "?" "[" ident "]"
@@ -780,7 +780,7 @@ numeral: [
 ]
 
 bigint: [
-| DELETE NUMERAL
+| DELETE NUMBER
 | num
 ]
 
@@ -797,7 +797,7 @@ ident: [
 | first_letter LIST0 subsequent_letter
 ]
 
-NUMERAL: [
+NUMBER: [
 | numeral
 ]
 
@@ -2210,7 +2210,7 @@ SPLICE: [
 | IDENT
 | LEFTQMARK
 | natural
-| NUMERAL
+| NUMBER
 | STRING
 | hyp
 | var
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index f628c86cf1..f82f196b36 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -162,7 +162,7 @@ appl_arg: [
 atomic_constr: [
 | global univ_instance
 | sort
-| NUMERAL
+| NUMBER
 | string
 | "_"
 | "?" "[" ident "]"
@@ -283,7 +283,7 @@ pattern0: [
 | "_"
 | "(" pattern200 ")"
 | "(" pattern200 "|" LIST1 pattern200 SEP "|" ")"
-| NUMERAL
+| NUMBER
 | string
 ]
 
@@ -440,12 +440,12 @@ natural: [
 ]
 
 bigint: [
-| NUMERAL
-| test_minus_nat "-" NUMERAL
+| NUMBER
+| test_minus_nat "-" NUMBER
 ]
 
 bignat: [
-| NUMERAL
+| NUMBER
 ]
 
 bar_cbrace: [
-- 
cgit v1.2.3


From f61d7d1139bd5f9e0efd34460e8daf68e454e46b Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 4 Sep 2020 15:06:00 +0200
Subject: [parsing] Simplify bigint

---
 doc/tools/docgram/common.edit_mlg | 5 +++--
 doc/tools/docgram/fullGrammar     | 4 ++--
 2 files changed, 5 insertions(+), 4 deletions(-)

(limited to 'doc/tools')

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index a619089cdd..549ace5d13 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -780,8 +780,9 @@ numeral: [
 ]
 
 bigint: [
-| DELETE NUMBER
-| num
+| DELETE bignat
+| REPLACE test_minus_nat "-" bignat
+| WITH OPT "-" bignat
 ]
 
 first_letter: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index f82f196b36..73b721702e 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -440,8 +440,8 @@ natural: [
 ]
 
 bigint: [
-| NUMBER
-| test_minus_nat "-" NUMBER
+| bignat
+| test_minus_nat "-" bignat
 ]
 
 bignat: [
-- 
cgit v1.2.3


From 46b9480a717d5ca78e354fa843f39eed87cb7b15 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 4 Sep 2020 15:08:00 +0200
Subject: [refman] Rename num to natural

---
 doc/tools/coqrst/coqdomain.py     |   6 +-
 doc/tools/docgram/common.edit_mlg |  27 ++++-----
 doc/tools/docgram/orderedGrammar  | 112 +++++++++++++++++++-------------------
 3 files changed, 70 insertions(+), 75 deletions(-)

(limited to 'doc/tools')

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index cffe196b77..3fef3bcbd1 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -351,7 +351,7 @@ class TacticObject(NotationObject):
 
     Example::
 
-       .. tacn:: do @num @expr
+       .. tacn:: do @natural @expr
 
           :token:`expr` is evaluated to ``v`` which must be a tactic value. …
     """
@@ -401,7 +401,7 @@ class OptionObject(NotationObject):
 
     Example::
 
-       .. opt:: Hyps Limit @num
+       .. opt:: Hyps Limit @natural
           :name Hyps Limit
 
           Controls the maximum number of hypotheses displayed in goals after
@@ -452,7 +452,7 @@ class ProductionObject(CoqObject):
 
     Example::
 
-        .. prodn:: occ_switch ::= { {? {| + | - } } {* @num } }
+        .. prodn:: occ_switch ::= { {? {| + | - } } {* @natural } }
         term += let: @pattern := @term in @term
         | second_production
 
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: [
-- 
cgit v1.2.3


From 754e138e1e1c86dcd5e9d07084a5d33a5056ce9d Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 4 Sep 2020 15:09:00 +0200
Subject: [refman] Rename numeral to number

---
 doc/tools/docgram/common.edit_mlg |  4 ++--
 doc/tools/docgram/orderedGrammar  | 10 +++++-----
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'doc/tools')

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index ff40555696..fbf83760ad 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -770,7 +770,7 @@ int: [
 | OPT "-" natural
 ]
 
-numeral: [
+number: [
 | OPT "-" decnat OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnat )
 | OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat )
 ]
@@ -795,7 +795,7 @@ ident: [
 ]
 
 NUMBER: [
-| numeral
+| number
 ]
 
 (* todo: QUOTATION only used in a test suite .mlg files, is it documented/useful? *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 6d07f6b0c4..a021bdbec0 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -93,7 +93,7 @@ term_explicit: [
 ]
 
 primitive_notations: [
-| numeral
+| number
 | string
 ]
 
@@ -129,7 +129,7 @@ type: [
 | term
 ]
 
-numeral: [
+number: [
 | OPT "-" decnat OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnat )
 | OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat )
 ]
@@ -429,7 +429,7 @@ pattern0: [
 | "{|" LIST0 ( qualid ":=" pattern ) "|}"
 | "_"
 | "(" LIST1 pattern SEP "|" ")"
-| numeral
+| number
 | string
 ]
 
@@ -1291,8 +1291,8 @@ field_mod: [
 ]
 
 numeral_modifier: [
-| "(" "warning" "after" numeral ")"
-| "(" "abstract" "after" numeral ")"
+| "(" "warning" "after" number ")"
+| "(" "abstract" "after" number ")"
 ]
 
 hints_path: [
-- 
cgit v1.2.3


From 724966f56caa66a5ddc9a992cf870ebc2efae004 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Mon, 7 Sep 2020 11:53:49 +0200
Subject: [refman] Rename int to integer

---
 doc/tools/docgram/common.edit_mlg | 42 ++++++++++++++++++---------------------
 doc/tools/docgram/fullGrammar     |  6 +++---
 doc/tools/docgram/orderedGrammar  | 38 +++++++++++++++++------------------
 3 files changed, 41 insertions(+), 45 deletions(-)

(limited to 'doc/tools')

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index fbf83760ad..89009764c8 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -736,11 +736,6 @@ export_token: [
 ]
 
 (* lexer stuff *)
-integer: [ | DELETENT ]
-RENAME: [
-| integer int (* todo: review uses in .mlg files, some should be "natural" *)
-]
-
 LEFTQMARK: [
 | "?"
 ]
@@ -766,8 +761,9 @@ natural: [
 | WITH [ decnat | hexnat ]
 ]
 
-int: [
-| OPT "-" natural
+integer: [
+| REPLACE bigint
+| WITH OPT "-" natural
 ]
 
 number: [
@@ -1091,13 +1087,13 @@ simple_tactic: [
 | WITH "subst" OPT ( LIST1 var )
 | DELETE "subst"
 | DELETE "congruence"
-| DELETE "congruence" int
+| DELETE "congruence" integer
 | DELETE "congruence" "with" LIST1 constr
-| REPLACE "congruence" int "with" LIST1 constr
-| WITH "congruence" OPT int OPT ( "with" LIST1 constr )
+| REPLACE "congruence" integer "with" LIST1 constr
+| WITH "congruence" OPT integer OPT ( "with" LIST1 constr )
 | DELETE "show" "ltac" "profile"
-| REPLACE "show" "ltac" "profile" "cutoff" int
-| WITH "show" "ltac" "profile" OPT [ "cutoff" int | string ]
+| REPLACE "show" "ltac" "profile" "cutoff" integer
+| WITH "show" "ltac" "profile" OPT [ "cutoff" integer | string ]
 | DELETE "show" "ltac" "profile" string
 (* perversely, the mlg uses "tactic3" instead of "tactic_expr3" *)
 | DELETE "transparent_abstract" tactic3
@@ -1205,11 +1201,11 @@ command: [
 | REPLACE "Next" "Obligation" "of" ident withtac
 | WITH "Next" "Obligation" OPT ( "of" ident ) withtac
 | DELETE "Next" "Obligation" withtac
-| REPLACE "Obligation" int "of" ident ":" lglob withtac
-| WITH "Obligation" int OPT ( "of" ident ) OPT ( ":" lglob withtac )
-| DELETE "Obligation" int "of" ident withtac
-| DELETE "Obligation" int ":" lglob withtac
-| DELETE "Obligation" int withtac
+| REPLACE "Obligation" integer "of" ident ":" lglob withtac
+| WITH "Obligation" integer OPT ( "of" ident ) OPT ( ":" lglob withtac )
+| DELETE "Obligation" integer "of" ident withtac
+| DELETE "Obligation" integer ":" lglob withtac
+| DELETE "Obligation" integer withtac
 | REPLACE "Obligations" "of" ident
 | WITH "Obligations" OPT ( "of" ident )
 | DELETE "Obligations"
@@ -1229,17 +1225,17 @@ command: [
 | DELETE "Show" ident
 | "Show" OPT [ ident | natural ]
 | DELETE "Show" "Ltac" "Profile"
-| REPLACE "Show" "Ltac" "Profile" "CutOff" int
-| WITH "Show" "Ltac" "Profile" OPT [ "CutOff" int | string ]
+| REPLACE "Show" "Ltac" "Profile" "CutOff" integer
+| WITH "Show" "Ltac" "Profile" OPT [ "CutOff" integer | string ]
 | DELETE "Show" "Ltac" "Profile" string
 | DELETE "Show" "Proof"  (* combined with Show Proof Diffs in vernac_toplevel *)
 | REPLACE "Solve" "All" "Obligations" "with" tactic
 | WITH "Solve" "All" "Obligations" OPT ( "with" tactic )
 | DELETE "Solve" "All" "Obligations"
-| REPLACE "Solve" "Obligation" int "of" ident "with" tactic
-| WITH "Solve" "Obligation" int OPT ( "of" ident ) "with" tactic
+| REPLACE "Solve" "Obligation" integer "of" ident "with" tactic
+| WITH "Solve" "Obligation" integer OPT ( "of" ident ) "with" tactic
 | DELETE "Solve" "Obligations"
-| DELETE "Solve" "Obligation" int "with" tactic
+| DELETE "Solve" "Obligation" integer "with" tactic
 | REPLACE "Solve" "Obligations" "of" ident "with" tactic
 | WITH "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" tactic )
 | DELETE "Solve" "Obligations" "with" tactic
@@ -2154,7 +2150,7 @@ tac2expr5: [
 
 RENAME: [
 | Prim.string string
-| Prim.integer int
+| Prim.integer integer
 | Prim.qualid qualid
 | Prim.natural natural
 ]
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 73b721702e..994447b12d 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -598,7 +598,7 @@ command: [
 | "Hint" "Cut" "[" hints_path "]" opthints
 | "Typeclasses" "Transparent" LIST0 reference
 | "Typeclasses" "Opaque" LIST0 reference
-| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT int
+| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT integer
 | "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ]
 | "Proof" "using" G_vernac.section_subset_expr OPT [ "with" Pltac.tactic ]
 | "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic
@@ -652,7 +652,7 @@ command: [
 | "Print" "Rewrite" "HintDb" preident
 | "Reset" "Ltac" "Profile"
 | "Show" "Ltac" "Profile"
-| "Show" "Ltac" "Profile" "CutOff" int
+| "Show" "Ltac" "Profile" "CutOff" integer
 | "Show" "Ltac" "Profile" string
 | "Show" "Lia" "Profile"      (* micromega plugin *)
 | "Add" "Zify" "InjTyp" constr      (* micromega plugin *)
@@ -1715,7 +1715,7 @@ simple_tactic: [
 | "stop" "ltac" "profiling"
 | "reset" "ltac" "profile"
 | "show" "ltac" "profile"
-| "show" "ltac" "profile" "cutoff" int
+| "show" "ltac" "profile" "cutoff" integer
 | "show" "ltac" "profile" string
 | "restart_timer" OPT string
 | "finish_timing" OPT string
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index a021bdbec0..105bd4668e 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -134,7 +134,7 @@ number: [
 | OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat )
 ]
 
-int: [
+integer: [
 | OPT "-" natural
 ]
 
@@ -514,7 +514,7 @@ occs_nums: [
 ]
 
 int_or_var: [
-| int
+| integer
 | ident
 ]
 
@@ -686,7 +686,7 @@ scope_key: [
 
 strategy_level: [
 | "opaque"
-| int
+| integer
 | "expand"
 | "transparent"
 ]
@@ -827,9 +827,9 @@ command: [
 | "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 ) )
+| "Obligation" integer OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) )
 | "Next" "Obligation" OPT ( "of" ident ) OPT ( "with" ltac_expr )
-| "Solve" "Obligation" int OPT ( "of" ident ) "with" ltac_expr
+| "Solve" "Obligation" integer OPT ( "of" ident ) "with" ltac_expr
 | "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" ltac_expr )
 | "Solve" "All" "Obligations" OPT ( "with" ltac_expr )
 | "Admit" "Obligations" OPT ( "of" ident )
@@ -852,7 +852,7 @@ command: [
 | "Optimize" "Proof"
 | "Optimize" "Heap"
 | "Reset" "Ltac" "Profile"
-| "Show" "Ltac" "Profile" OPT [ "CutOff" int | string ]
+| "Show" "Ltac" "Profile" OPT [ "CutOff" integer | string ]
 | "Show" "Lia" "Profile"      (* micromega plugin *)
 | "Add" "Zify" "InjTyp" one_term      (* micromega plugin *)
 | "Add" "Zify" "BinOp" one_term      (* micromega plugin *)
@@ -891,7 +891,7 @@ command: [
 | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
 | "Typeclasses" "Transparent" LIST0 qualid
 | "Typeclasses" "Opaque" LIST0 qualid
-| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" eauto_search_strategy_name ")" ) OPT int
+| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" eauto_search_strategy_name ")" ) OPT integer
 | "Proof" "with" ltac_expr OPT [ "using" section_subset_expr ]
 | "Proof" "using" section_subset_expr OPT [ "with" ltac_expr ]
 | "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr
@@ -964,7 +964,7 @@ command: [
 | "Arguments" reference LIST0 arg_specs LIST0 [ "," LIST0 implicits_alt ] OPT [ ":" LIST1 args_modifier SEP "," ]
 | "Implicit" [ "Type" | "Types" ] reserv_list
 | "Generalizable" [ [ "Variable" | "Variables" ] LIST1 ident | "All" "Variables" | "No" "Variables" ]
-| "Set" setting_name OPT [ int | string ]
+| "Set" setting_name OPT [ integer | string ]
 | "Unset" setting_name
 | "Open" "Scope" scope
 | "Close" "Scope" scope
@@ -988,7 +988,7 @@ command: [
 | "Ltac2" OPT "mutable" OPT "rec" tac2def_body LIST0 ( "with" tac2def_body )
 | "Ltac2" "Type" OPT "rec" tac2typ_def LIST0 ( "with" tac2typ_def )
 | "Ltac2" "@" "external" ident ":" ltac2_type ":=" string string
-| "Ltac2" "Notation" LIST1 ltac2_scope OPT ( ":" int ) ":=" ltac2_expr
+| "Ltac2" "Notation" LIST1 ltac2_scope OPT ( ":" integer ) ":=" ltac2_expr
 | "Ltac2" "Set" qualid OPT [ "as" ident ] ":=" ltac2_expr
 | "Ltac2" "Notation" [ string | lident ] ":=" ltac2_expr      (* Ltac2 plugin *)
 | "Ltac2" "Eval" ltac2_expr      (* Ltac2 plugin *)
@@ -1255,7 +1255,7 @@ qhyp: [
 
 int_or_id: [
 | ident
-| int      (* extraction plugin *)
+| integer      (* extraction plugin *)
 ]
 
 language: [
@@ -1417,8 +1417,8 @@ simple_tactic: [
 | "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2
 | "first" "[" LIST0 ltac_expr SEP "|" "]"
 | "solve" "[" LIST0 ltac_expr SEP "|" "]"
-| "idtac" LIST0 [ ident | string | int ]
-| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | int ]
+| "idtac" LIST0 [ ident | string | integer ]
+| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | integer ]
 | "fun" LIST1 name "=>" ltac_expr
 | "eval" red_expr "in" term
 | "context" ident "[" term "]"
@@ -1462,7 +1462,7 @@ simple_tactic: [
 | "evar" "(" ident ":" term ")"
 | "evar" one_term
 | "instantiate" "(" ident ":=" term ")"
-| "instantiate" "(" int ":=" term ")" OPT hloc
+| "instantiate" "(" integer ":=" term ")" OPT hloc
 | "instantiate"
 | "stepl" one_term OPT ( "by" ltac_expr )
 | "stepr" one_term OPT ( "by" ltac_expr )
@@ -1501,7 +1501,7 @@ simple_tactic: [
 | "start" "ltac" "profiling"
 | "stop" "ltac" "profiling"
 | "reset" "ltac" "profile"
-| "show" "ltac" "profile" OPT [ "cutoff" int | string ]
+| "show" "ltac" "profile" OPT [ "cutoff" integer | string ]
 | "restart_timer" OPT string
 | "finish_timing" OPT ( "(" string ")" ) OPT string
 | "eassumption"
@@ -1606,7 +1606,7 @@ simple_tactic: [
 | "change_no_check" conversion OPT clause_dft_concl
 | "btauto"
 | "rtauto"
-| "congruence" OPT int OPT ( "with" LIST1 one_term )
+| "congruence" OPT integer OPT ( "with" LIST1 one_term )
 | "f_equal"
 | "firstorder" OPT ltac_expr firstorder_rhs
 | "gintuition" OPT ltac_expr
@@ -2035,7 +2035,7 @@ tac2rec_field: [
 
 ltac2_scope: [
 | string      (* Ltac2 plugin *)
-| int      (* Ltac2 plugin *)
+| integer      (* Ltac2 plugin *)
 | name      (* Ltac2 plugin *)
 | name "(" LIST1 ltac2_scope SEP "," ")"      (* Ltac2 plugin *)
 ]
@@ -2085,7 +2085,7 @@ ltac2_expr0: [
 ]
 
 ltac2_tactic_atom: [
-| int      (* Ltac2 plugin *)
+| integer      (* Ltac2 plugin *)
 | string      (* Ltac2 plugin *)
 | qualid      (* Ltac2 plugin *)
 | "@" ident      (* Ltac2 plugin *)
@@ -2201,7 +2201,7 @@ with_names: [
 ]
 
 occurrences: [
-| LIST1 int
+| LIST1 integer
 | ident
 ]
 
@@ -2296,7 +2296,7 @@ ltac_expr0: [
 ]
 
 tactic_atom: [
-| int
+| integer
 | qualid
 | "()"
 ]
-- 
cgit v1.2.3


From 031cc2ba1a19a06766df85b8693c72f16fa62de6 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Mon, 7 Sep 2020 12:07:23 +0200
Subject: [refman] Explicit integer and natural

As respectively bigint and bignat that fit into an OCaml int.
---
 doc/tools/docgram/common.edit_mlg |  6 ++----
 doc/tools/docgram/orderedGrammar  | 12 ++++++++++--
 2 files changed, 12 insertions(+), 6 deletions(-)

(limited to 'doc/tools')

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 89009764c8..ea60fa22d6 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -756,8 +756,8 @@ hexnat: [
 | [ "0x" | "0X" ] hexdigit LIST0 [ hexdigit | "_" ]
 ]
 
-natural: [
-| REPLACE bignat
+bignat: [
+| REPLACE NUMBER
 | WITH [ decnat | hexnat ]
 ]
 
@@ -2197,7 +2197,6 @@ ltac2_induction_clause: [
 SPLICE: [
 | clause
 | noedit_mode
-| bigint
 | match_list
 | match_context_list
 | IDENT
@@ -2360,7 +2359,6 @@ SPLICE: [
 | search_queries
 | locatable
 | scope_delimiter
-| bignat
 | one_import_filter_name
 | search_where
 | message_token
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 105bd4668e..8d4e0189e6 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -139,6 +139,14 @@ integer: [
 ]
 
 natural: [
+| bignat
+]
+
+bigint: [
+| OPT "-" bignat
+]
+
+bignat: [
 | [ decnat | hexnat ]
 ]
 
@@ -1291,8 +1299,8 @@ field_mod: [
 ]
 
 numeral_modifier: [
-| "(" "warning" "after" number ")"
-| "(" "abstract" "after" number ")"
+| "(" "warning" "after" bignat ")"
+| "(" "abstract" "after" bignat ")"
 ]
 
 hints_path: [
-- 
cgit v1.2.3


From 92bc869c2cec1ffb7e2d0bfcc6b64147718fbe87 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 8 Sep 2020 10:41:03 +0200
Subject: Turn integer into natural in several mlgs

Negative values had no meaning there.
Those were spotted by Hugo Herbelin while reviewing #12979 .
---
 doc/tools/docgram/common.edit_mlg | 16 ++++++++--------
 doc/tools/docgram/fullGrammar     | 16 ++++++++--------
 doc/tools/docgram/orderedGrammar  | 10 +++++-----
 3 files changed, 21 insertions(+), 21 deletions(-)

(limited to 'doc/tools')

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index ea60fa22d6..66b6ffac89 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1201,11 +1201,11 @@ command: [
 | REPLACE "Next" "Obligation" "of" ident withtac
 | WITH "Next" "Obligation" OPT ( "of" ident ) withtac
 | DELETE "Next" "Obligation" withtac
-| REPLACE "Obligation" integer "of" ident ":" lglob withtac
-| WITH "Obligation" integer OPT ( "of" ident ) OPT ( ":" lglob withtac )
-| DELETE "Obligation" integer "of" ident withtac
-| DELETE "Obligation" integer ":" lglob withtac
-| DELETE "Obligation" integer withtac
+| REPLACE "Obligation" natural "of" ident ":" lglob withtac
+| WITH "Obligation" natural OPT ( "of" ident ) OPT ( ":" lglob withtac )
+| DELETE "Obligation" natural "of" ident withtac
+| DELETE "Obligation" natural ":" lglob withtac
+| DELETE "Obligation" natural withtac
 | REPLACE "Obligations" "of" ident
 | WITH "Obligations" OPT ( "of" ident )
 | DELETE "Obligations"
@@ -1232,10 +1232,10 @@ command: [
 | REPLACE "Solve" "All" "Obligations" "with" tactic
 | WITH "Solve" "All" "Obligations" OPT ( "with" tactic )
 | DELETE "Solve" "All" "Obligations"
-| REPLACE "Solve" "Obligation" integer "of" ident "with" tactic
-| WITH "Solve" "Obligation" integer OPT ( "of" ident ) "with" tactic
+| REPLACE "Solve" "Obligation" natural "of" ident "with" tactic
+| WITH "Solve" "Obligation" natural OPT ( "of" ident ) "with" tactic
 | DELETE "Solve" "Obligations"
-| DELETE "Solve" "Obligation" integer "with" tactic
+| DELETE "Solve" "Obligation" natural "with" tactic
 | REPLACE "Solve" "Obligations" "of" ident "with" tactic
 | WITH "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" tactic )
 | DELETE "Solve" "Obligations" "with" tactic
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 994447b12d..9614fc06fe 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -606,14 +606,14 @@ command: [
 | "Locate" "Ltac" reference
 | "Ltac" LIST1 ltac_tacdef_body SEP "with"
 | "Print" "Ltac" "Signatures"
-| "Obligation" integer "of" ident ":" lglob withtac
-| "Obligation" integer "of" ident withtac
-| "Obligation" integer ":" lglob withtac
-| "Obligation" integer withtac
+| "Obligation" natural "of" ident ":" lglob withtac
+| "Obligation" natural "of" ident withtac
+| "Obligation" natural ":" lglob withtac
+| "Obligation" natural withtac
 | "Next" "Obligation" "of" ident withtac
 | "Next" "Obligation" withtac
-| "Solve" "Obligation" integer "of" ident "with" tactic
-| "Solve" "Obligation" integer "with" tactic
+| "Solve" "Obligation" natural "of" ident "with" tactic
+| "Solve" "Obligation" natural "with" tactic
 | "Solve" "Obligations" "of" ident "with" tactic
 | "Solve" "Obligations" "with" tactic
 | "Solve" "Obligations"
@@ -2099,7 +2099,7 @@ match_list: [
 message_token: [
 | identref
 | STRING
-| integer
+| natural
 ]
 
 ltac_def_kind: [
@@ -2811,7 +2811,7 @@ sexpr: [
 
 syn_level: [
 |      (* Ltac2 plugin *)
-| ":" Prim.integer      (* Ltac2 plugin *)
+| ":" Prim.natural      (* Ltac2 plugin *)
 ]
 
 tac2def_syn: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 8d4e0189e6..bbc4edf199 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -835,9 +835,9 @@ command: [
 | "Comments" LIST0 [ one_term | string | natural ]
 | "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info
 | "Declare" "Scope" scope_name
-| "Obligation" integer OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) )
+| "Obligation" natural OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) )
 | "Next" "Obligation" OPT ( "of" ident ) OPT ( "with" ltac_expr )
-| "Solve" "Obligation" integer OPT ( "of" ident ) "with" ltac_expr
+| "Solve" "Obligation" natural OPT ( "of" ident ) "with" ltac_expr
 | "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" ltac_expr )
 | "Solve" "All" "Obligations" OPT ( "with" ltac_expr )
 | "Admit" "Obligations" OPT ( "of" ident )
@@ -996,7 +996,7 @@ command: [
 | "Ltac2" OPT "mutable" OPT "rec" tac2def_body LIST0 ( "with" tac2def_body )
 | "Ltac2" "Type" OPT "rec" tac2typ_def LIST0 ( "with" tac2typ_def )
 | "Ltac2" "@" "external" ident ":" ltac2_type ":=" string string
-| "Ltac2" "Notation" LIST1 ltac2_scope OPT ( ":" integer ) ":=" ltac2_expr
+| "Ltac2" "Notation" LIST1 ltac2_scope OPT ( ":" natural ) ":=" ltac2_expr
 | "Ltac2" "Set" qualid OPT [ "as" ident ] ":=" ltac2_expr
 | "Ltac2" "Notation" [ string | lident ] ":=" ltac2_expr      (* Ltac2 plugin *)
 | "Ltac2" "Eval" ltac2_expr      (* Ltac2 plugin *)
@@ -1425,8 +1425,8 @@ simple_tactic: [
 | "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2
 | "first" "[" LIST0 ltac_expr SEP "|" "]"
 | "solve" "[" LIST0 ltac_expr SEP "|" "]"
-| "idtac" LIST0 [ ident | string | integer ]
-| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | integer ]
+| "idtac" LIST0 [ ident | string | natural ]
+| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | natural ]
 | "fun" LIST1 name "=>" ltac_expr
 | "eval" red_expr "in" term
 | "context" ident "[" term "]"
-- 
cgit v1.2.3


From d5eb564a1ae46409e90a2c6bd6af5b77aa37773e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 9 Sep 2020 20:24:46 +0200
Subject: Adding a wit_natural standard argument.

---
 doc/tools/docgram/common.edit_mlg | 6 +++---
 doc/tools/docgram/fullGrammar     | 5 +++--
 doc/tools/docgram/orderedGrammar  | 3 ++-
 3 files changed, 8 insertions(+), 6 deletions(-)

(limited to 'doc/tools')

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 66b6ffac89..a22f7ae9f3 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1087,10 +1087,10 @@ simple_tactic: [
 | WITH "subst" OPT ( LIST1 var )
 | DELETE "subst"
 | DELETE "congruence"
-| DELETE "congruence" integer
+| DELETE "congruence" natural
 | DELETE "congruence" "with" LIST1 constr
-| REPLACE "congruence" integer "with" LIST1 constr
-| WITH "congruence" OPT integer OPT ( "with" LIST1 constr )
+| REPLACE "congruence" natural "with" LIST1 constr
+| WITH "congruence" OPT natural OPT ( "with" LIST1 constr )
 | DELETE "show" "ltac" "profile"
 | REPLACE "show" "ltac" "profile" "cutoff" integer
 | WITH "show" "ltac" "profile" OPT [ "cutoff" integer | string ]
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 9614fc06fe..2ee8e4347e 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -689,6 +689,7 @@ command: [
 | "Print" "Rings"      (* setoid_ring plugin *)
 | "Add" "Field" ident ":" constr OPT field_mods      (* setoid_ring plugin *)
 | "Print" "Fields"      (* setoid_ring plugin *)
+| "Number" "Notation" reference reference reference ":" ident numnotoption
 | "Numeral" "Notation" reference reference reference ":" ident numnotoption
 | "String" "Notation" reference reference reference ":" ident
 | "Ltac2" ltac2_entry      (* Ltac2 plugin *)
@@ -1435,9 +1436,9 @@ constr_as_binder_kind: [
 simple_tactic: [
 | "btauto"
 | "congruence"
-| "congruence" integer
+| "congruence" natural
 | "congruence" "with" LIST1 constr
-| "congruence" integer "with" LIST1 constr
+| "congruence" natural "with" LIST1 constr
 | "f_equal"
 | "firstorder" OPT tactic firstorder_using
 | "firstorder" OPT tactic "with" LIST1 preident
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index bbc4edf199..aae96fc966 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -896,6 +896,7 @@ command: [
 | "Print" "Rings"      (* setoid_ring plugin *)
 | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* setoid_ring plugin *)
 | "Print" "Fields"      (* setoid_ring plugin *)
+| "Number" "Notation" qualid qualid qualid ":" ident OPT numeral_modifier
 | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
 | "Typeclasses" "Transparent" LIST0 qualid
 | "Typeclasses" "Opaque" LIST0 qualid
@@ -1614,7 +1615,7 @@ simple_tactic: [
 | "change_no_check" conversion OPT clause_dft_concl
 | "btauto"
 | "rtauto"
-| "congruence" OPT integer OPT ( "with" LIST1 one_term )
+| "congruence" OPT natural OPT ( "with" LIST1 one_term )
 | "f_equal"
 | "firstorder" OPT ltac_expr firstorder_rhs
 | "gintuition" OPT ltac_expr
-- 
cgit v1.2.3