Merge PR #13417: Use nat_or_var in grammar where negative values don't make sense

Reviewed-by: Zimmi48

23 files changed, 134 insertions, 109 deletions

diff --git a/doc/changelog/04-tactics/13417-no_int_or_var.rst b/doc/changelog/04-tactics/13417-no_int_or_var.rst
new file mode 100644
index 0000000000..667ee28eea
--- /dev/null
+++ b/doc/changelog/04-tactics/13417-no_int_or_var.rst
@@ -0,0 +1,7 @@
+- **Removed:**
+  A number of tactics that formerly accepted negative
+  numbers as parameters now give syntax errors for negative
+  values.  These include {e}constructor, do, timeout,
+  9 {e}auto tactics and psatz*.
+  (`#13417 <https://github.com/coq/coq/pull/13417>`_,
+  by Jim Fehrle).
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index fb9965e43a..28b60878d2 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -250,11 +250,11 @@ proof by abstracting monomials by variables.
 `psatz`: a proof procedure for non-linear arithmetic
 ----------------------------------------------------
 
-.. tacn:: psatz @one_term {? @int_or_var }
+.. tacn:: psatz @one_term {? @nat_or_var }
    :name: psatz
 
    This tactic explores the *Cone* by increasing degrees – hence the
-   depth parameter *n*. In theory, such a proof search is complete – if the
+   depth parameter :token:`nat_or_var`. In theory, such a proof search is complete – if the
    goal is provable the search eventually stops. Unfortunately, the
    external oracle is using numeric (approximate) optimization techniques
    that might miss a refutation.
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 22527dc379..98445fca1a 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -405,7 +405,7 @@ Summary of the commands
    Shows the list of instances associated with the typeclass :token:`reference`.
 
 
-.. tacn:: typeclasses eauto {? bfs } {? @int_or_var } {? with {+ @ident } }
+.. tacn:: typeclasses eauto {? bfs } {? @nat_or_var } {? with {+ @ident } }
 
    This proof search tactic uses the resolution engine that is run
    implicitly during type checking. This tactic uses a different resolution
@@ -445,11 +445,11 @@ Summary of the commands
    + Use the :cmd:`Typeclasses eauto` command to customize the behavior of
      this tactic.
 
-   :n:`@int_or_var`
+   :n:`@nat_or_var`
      Specifies the maximum depth of the search.
 
       .. warning::
-         The semantics for the limit :n:`@int_or_var`
+         The semantics for the limit :n:`@nat_or_var`
          are different than for :tacn:`auto`. By default, if no limit is given, the
          search is unbounded. Unlike :tacn:`auto`, introduction steps count against
          the limit, which might result in larger limits being necessary when
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 6464f085b8..2fc3c9f748 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -480,15 +480,15 @@ separately.  They succeed only if there is a success for each goal.  For example
 Do loop
 ~~~~~~~
 
-.. tacn:: do @int_or_var @ltac_expr3
+.. tacn:: do @nat_or_var @ltac_expr3
    :name: do
 
-   The do loop repeats a tactic :token:`int_or_var` times:
+   The do loop repeats a tactic :token:`nat_or_var` times:
 
-   :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. This tactic
-   value ``v`` is applied :token:`int_or_var` times. Supposing :token:`int_or_var` > 1, after the
+   :n:`@ltac_expr` is evaluated to ``v``, which must be a tactic value. This tactic
+   value ``v`` is applied :token:`nat_or_var` times. If :token:`nat_or_var` > 1, after the
    first application of ``v``, ``v`` is applied, at least once, to the generated
-   subgoals and so on. It fails if the application of ``v`` fails before :token:`int_or_var`
+   subgoals and so on. It fails if the application of ``v`` fails before :token:`nat_or_var`
    applications have been completed.
 
    :tacn:`do` is an :token:`l3_tactic`.
@@ -973,11 +973,11 @@ Timeout
 We can force a tactic to stop if it has not finished after a certain
 amount of time:
 
-.. tacn:: timeout @int_or_var @ltac_expr3
+.. tacn:: timeout @nat_or_var @ltac_expr3
    :name: timeout
 
    :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value
-   ``v`` is applied normally, except that it is interrupted after :n:`@natural` seconds
+   ``v`` is applied normally, except that it is interrupted after :n:`@nat_or_var` seconds
    if it is still running. In this case the outcome is a failure.
 
    :tacn:`timeout` is an :token:`l3_tactic`.
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 5283f60b11..9ec568c2c7 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -323,10 +323,12 @@ Performing computations
    | delta {? @delta_flag }
    ref_or_pattern_occ ::= @reference {? at @occs_nums }
    | @one_term {? at @occs_nums }
-   occs_nums ::= {+ {| @natural | @ident } }
-   | - {+ {| @natural | @ident } }
+   occs_nums ::= {+ @nat_or_var }
+   | - {+ @nat_or_var }
    int_or_var ::= @integer
    | @ident
+   nat_or_var ::= @natural
+   | @ident
    unfold_occ ::= @reference {? at @occs_nums }
    pattern_occ ::= @one_term {? at @occs_nums }
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 816acba4c1..4080eaae08 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -815,7 +815,10 @@ ltac_expr3: [
 | REPLACE "abstract" ltac_expr2 "using" ident
 | WITH "abstract" ltac_expr2 OPT ( "using" ident )
 | l3_tactic
-| EDIT "do" ADD_OPT int_or_var ssrmmod ssrdotac ssrclauses  TAG SSR
+(* | EDIT "do" ADD_OPT nat_or_var ssrmmod ssrdotac ssrclauses  TAG SSR *)
+| DELETE "do" ssrmmod ssrdotac ssrclauses      (* SSR plugin *)
+| DELETE "do" ssrortacarg ssrclauses      (* SSR plugin *)
+| DELETE "do" nat_or_var ssrmmod ssrdotac ssrclauses      (* SSR plugin *)
 | MOVEALLBUT ltac_builtins
 | l3_tactic
 | ltac_expr2
@@ -917,13 +920,13 @@ simple_tactic: [
 | REPLACE "cofix" ident "with" LIST1 cofixdecl
 | WITH "cofix" ident OPT ( "with" LIST1 cofixdecl )
 | DELETE "constructor"
-| DELETE "constructor" int_or_var
-| REPLACE "constructor" int_or_var "with" bindings
-| WITH "constructor" OPT int_or_var OPT ( "with" bindings )
+| DELETE "constructor" nat_or_var
+| REPLACE "constructor" nat_or_var "with" bindings
+| WITH "constructor" OPT nat_or_var OPT ( "with" bindings )
 | DELETE "econstructor"
-| DELETE "econstructor" int_or_var
-| REPLACE "econstructor" int_or_var "with" bindings
-| WITH "econstructor" OPT ( int_or_var OPT ( "with" bindings ) )
+| DELETE "econstructor" nat_or_var
+| REPLACE "econstructor" nat_or_var "with" bindings
+| WITH "econstructor" OPT ( nat_or_var OPT ( "with" bindings ) )
 | DELETE "dependent" "rewrite" orient constr
 | REPLACE "dependent" "rewrite" orient constr "in" hyp
 | WITH "dependent" "rewrite" orient constr OPT ( "in" hyp )
@@ -1042,12 +1045,12 @@ simple_tactic: [
 | DELETE "finish_timing" OPT string
 | REPLACE "finish_timing" "(" string ")" OPT string
 | WITH "finish_timing" OPT ( "(" string ")" ) OPT string
-| REPLACE "hresolve_core" "(" ident ":=" constr ")" "at" int_or_var "in" constr
-| WITH "hresolve_core" "(" ident ":=" constr ")" OPT ( "at" int_or_var ) "in" constr
+| REPLACE "hresolve_core" "(" ident ":=" constr ")" "at" nat_or_var "in" constr
+| WITH "hresolve_core" "(" ident ":=" constr ")" OPT ( "at" nat_or_var ) "in" constr
 | DELETE "hresolve_core" "(" ident ":=" constr ")" "in" constr
-| EDIT "psatz_R" ADD_OPT int_or_var tactic
-| EDIT "psatz_Q" ADD_OPT int_or_var tactic
-| EDIT "psatz_Z" ADD_OPT int_or_var tactic
+| EDIT "psatz_R" ADD_OPT nat_or_var tactic
+| EDIT "psatz_Q" ADD_OPT nat_or_var tactic
+| EDIT "psatz_Z" ADD_OPT nat_or_var tactic
 | REPLACE "subst" LIST1 hyp
 | WITH "subst" LIST0 hyp
 | DELETE "subst"
@@ -1064,11 +1067,11 @@ simple_tactic: [
 | DELETE "transparent_abstract" tactic3
 | REPLACE "transparent_abstract" tactic3 "using" ident
 | WITH "transparent_abstract" ltac_expr3 OPT ( "using" ident )
-| "typeclasses" "eauto" OPT "bfs" OPT int_or_var OPT ( "with" LIST1 preident )
-| DELETE "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident
-| DELETE "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident
-| DELETE "typeclasses" "eauto" "bfs" OPT int_or_var
-| DELETE "typeclasses" "eauto" OPT int_or_var
+| "typeclasses" "eauto" OPT "bfs" OPT nat_or_var OPT ( "with" LIST1 preident )
+| DELETE "typeclasses" "eauto" "bfs" OPT nat_or_var "with" LIST1 preident
+| DELETE "typeclasses" "eauto" OPT nat_or_var "with" LIST1 preident
+| DELETE "typeclasses" "eauto" "bfs" OPT nat_or_var
+| DELETE "typeclasses" "eauto" OPT nat_or_var
 (* in Tactic Notation: *)
 | "setoid_replace" constr "with" constr OPT ( "using" "relation" constr ) OPT ( "in" hyp )
        OPT ( "at" LIST1 int_or_var ) OPT ( "by" ltac_expr3 )
@@ -1789,7 +1792,7 @@ tactic_notation_tactics: [
 | "field_simplify_eq" OPT ( "[" LIST1 constr "]" ) OPT ( "in" ident )
 | "intuition" OPT ltac_expr5  (* todo: Not too keen on things like "with_power_flags" in tauto.ml, not easy to follow *)
 | "nsatz" OPT ( "with" "radicalmax" ":=" constr "strategy" ":=" constr "parameters" ":=" constr "variables" ":=" constr )
-| "psatz" constr OPT int_or_var
+| "psatz" constr OPT nat_or_var
 | "ring" OPT ( "[" LIST1 constr "]" )
 | "ring_simplify" OPT ( "[" LIST1 constr "]" ) LIST1 constr OPT ( "in" ident )  (* todo: ident was "hyp", worth keeping? *)
 ]
@@ -2536,7 +2539,6 @@ SPLICE: [
 | by_arg_tac
 | by_tactic
 | quantified_hypothesis
-| nat_or_var
 | in_hyp_list
 | rename
 | export_token
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 03a20d621b..cdee623850 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1479,11 +1479,11 @@ simple_tactic: [
 | "right" "with" bindings
 | "eright" "with" bindings
 | "constructor"
-| "constructor" int_or_var
-| "constructor" int_or_var "with" bindings
+| "constructor" nat_or_var
+| "constructor" nat_or_var "with" bindings
 | "econstructor"
-| "econstructor" int_or_var
-| "econstructor" int_or_var "with" bindings
+| "econstructor" nat_or_var
+| "econstructor" nat_or_var "with" bindings
 | "specialize" constr_with_bindings
 | "specialize" constr_with_bindings "as" simple_intropattern
 | "symmetry"
@@ -1582,9 +1582,9 @@ simple_tactic: [
 | "generalize_eqs_vars" hyp
 | "dependent" "generalize_eqs_vars" hyp
 | "specialize_eqs" hyp
-| "hresolve_core" "(" ident ":=" constr ")" "at" int_or_var "in" constr
+| "hresolve_core" "(" ident ":=" constr ")" "at" nat_or_var "in" constr
 | "hresolve_core" "(" ident ":=" constr ")" "in" constr
-| "hget_evar" int_or_var
+| "hget_evar" nat_or_var
 | "destauto"
 | "destauto" "in" hyp
 | "transparent_abstract" tactic3
@@ -1617,25 +1617,25 @@ simple_tactic: [
 | "trivial" auto_using hintbases
 | "info_trivial" auto_using hintbases
 | "debug" "trivial" auto_using hintbases
-| "auto" OPT int_or_var auto_using hintbases
-| "info_auto" OPT int_or_var auto_using hintbases
-| "debug" "auto" OPT int_or_var auto_using hintbases
-| "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
-| "new" "auto" OPT int_or_var auto_using hintbases
-| "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
-| "info_eauto" OPT int_or_var OPT int_or_var auto_using hintbases
-| "dfs" "eauto" OPT int_or_var auto_using hintbases
-| "bfs" "eauto" OPT int_or_var auto_using hintbases
+| "auto" OPT nat_or_var auto_using hintbases
+| "info_auto" OPT nat_or_var auto_using hintbases
+| "debug" "auto" OPT nat_or_var auto_using hintbases
+| "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases
+| "new" "auto" OPT nat_or_var auto_using hintbases
+| "debug" "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases
+| "info_eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases
+| "dfs" "eauto" OPT nat_or_var auto_using hintbases
+| "bfs" "eauto" OPT nat_or_var auto_using hintbases
 | "autounfold" hintbases clause_dft_concl
 | "autounfold_one" hintbases "in" hyp
 | "autounfold_one" hintbases
 | "unify" constr constr
 | "unify" constr constr "with" preident
 | "convert_concl_no_check" constr
-| "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident
-| "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident
-| "typeclasses" "eauto" "bfs" OPT int_or_var
-| "typeclasses" "eauto" OPT int_or_var
+| "typeclasses" "eauto" "bfs" OPT nat_or_var "with" LIST1 preident
+| "typeclasses" "eauto" OPT nat_or_var "with" LIST1 preident
+| "typeclasses" "eauto" "bfs" OPT nat_or_var
+| "typeclasses" "eauto" OPT nat_or_var
 | "head_of_constr" ident constr
 | "not_evar" constr
 | "is_ground" constr
@@ -1734,7 +1734,7 @@ simple_tactic: [
 | "restart_timer" OPT string
 | "finish_timing" OPT string
 | "finish_timing" "(" string ")" OPT string
-| "psatz_Z" int_or_var tactic      (* micromega plugin *)
+| "psatz_Z" nat_or_var tactic      (* micromega plugin *)
 | "psatz_Z" tactic      (* micromega plugin *)
 | "xlia" tactic      (* micromega plugin *)
 | "xnlia" tactic      (* micromega plugin *)
@@ -1745,9 +1745,9 @@ simple_tactic: [
 | "sos_R" tactic      (* micromega plugin *)
 | "lra_Q" tactic      (* micromega plugin *)
 | "lra_R" tactic      (* micromega plugin *)
-| "psatz_R" int_or_var tactic      (* micromega plugin *)
+| "psatz_R" nat_or_var tactic      (* micromega plugin *)
 | "psatz_R" tactic      (* micromega plugin *)
-| "psatz_Q" int_or_var tactic      (* micromega plugin *)
+| "psatz_Q" nat_or_var tactic      (* micromega plugin *)
 | "psatz_Q" tactic      (* micromega plugin *)
 | "zify_iter_specs"      (* micromega plugin *)
 | "zify_op"      (* micromega plugin *)
@@ -2022,8 +2022,8 @@ ltac_expr4: [
 
 ltac_expr3: [
 | "try" ltac_expr3
-| "do" int_or_var ltac_expr3
-| "timeout" int_or_var ltac_expr3
+| "do" nat_or_var ltac_expr3
+| "timeout" nat_or_var ltac_expr3
 | "time" OPT string ltac_expr3
 | "repeat" ltac_expr3
 | "progress" ltac_expr3
@@ -2036,7 +2036,7 @@ ltac_expr3: [
 | ltac_expr2
 | "do" ssrmmod ssrdotac ssrclauses      (* SSR plugin *)
 | "do" ssrortacarg ssrclauses      (* SSR plugin *)
-| "do" int_or_var ssrmmod ssrdotac ssrclauses      (* SSR plugin *)
+| "do" nat_or_var ssrmmod ssrdotac ssrclauses      (* SSR plugin *)
 | "abstract" ssrdgens      (* SSR plugin *)
 ]
 
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 0209cf762a..c27169d432 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -652,8 +652,8 @@ ref_or_pattern_occ: [
 ]
 
 occs_nums: [
-| LIST1 [ natural | ident ]
-| "-" LIST1 [ natural | ident ]
+| LIST1 nat_or_var
+| "-" LIST1 nat_or_var
 ]
 
 int_or_var: [
@@ -661,6 +661,11 @@ int_or_var: [
 | ident
 ]
 
+nat_or_var: [
+| natural
+| ident
+]
+
 unfold_occ: [
 | reference OPT ( "at" occs_nums )
 ]
@@ -1620,8 +1625,8 @@ simple_tactic: [
 | "eleft" OPT ( "with" bindings )
 | "right" OPT ( "with" bindings )
 | "eright" OPT ( "with" bindings )
-| "constructor" OPT int_or_var OPT ( "with" bindings )
-| "econstructor" OPT ( int_or_var OPT ( "with" bindings ) )
+| "constructor" OPT nat_or_var OPT ( "with" bindings )
+| "econstructor" OPT ( nat_or_var OPT ( "with" bindings ) )
 | "specialize" one_term OPT ( "with" bindings ) OPT ( "as" simple_intropattern )
 | "symmetry" OPT ( "in" in_clause )
 | "split" OPT ( "with" bindings )
@@ -1648,8 +1653,8 @@ simple_tactic: [
 | bullet
 | "}"
 | "try" ltac_expr3
-| "do" int_or_var ltac_expr3
-| "timeout" int_or_var ltac_expr3
+| "do" nat_or_var ltac_expr3
+| "timeout" nat_or_var ltac_expr3
 | "time" OPT string ltac_expr3
 | "repeat" ltac_expr3
 | "progress" ltac_expr3
@@ -1658,8 +1663,6 @@ simple_tactic: [
 | "infoH" ltac_expr3
 | "abstract" ltac_expr2 OPT ( "using" ident )
 | "only" selector ":" ltac_expr3
-| "do" "[" ssrortacs "]" OPT ssr_in      (* SSR plugin *)
-| "do" OPT int_or_var ssrmmod [ ltac_expr3 | "[" ssrortacs "]"      (* SSR plugin *) ] OPT ssr_in      (* SSR plugin *)
 | "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2
 | "first" "[" LIST0 ltac_expr SEP "|" "]"
 | "solve" "[" LIST0 ltac_expr SEP "|" "]"
@@ -1718,8 +1721,8 @@ simple_tactic: [
 | "generalize_eqs_vars" ident
 | "dependent" "generalize_eqs_vars" ident
 | "specialize_eqs" ident
-| "hresolve_core" "(" ident ":=" one_term ")" OPT ( "at" int_or_var ) "in" one_term
-| "hget_evar" int_or_var
+| "hresolve_core" "(" ident ":=" one_term ")" OPT ( "at" nat_or_var ) "in" one_term
+| "hget_evar" nat_or_var
 | "destauto" OPT ( "in" ident )
 | "transparent_abstract" ltac_expr3 OPT ( "using" ident )
 | "constr_eq" one_term one_term
@@ -1756,20 +1759,20 @@ simple_tactic: [
 | "trivial" OPT auto_using OPT hintbases
 | "info_trivial" OPT auto_using OPT hintbases
 | "debug" "trivial" OPT auto_using OPT hintbases
-| "auto" OPT int_or_var OPT auto_using OPT hintbases
-| "info_auto" OPT int_or_var OPT auto_using OPT hintbases
-| "debug" "auto" OPT int_or_var OPT auto_using OPT hintbases
-| "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases
-| "new" "auto" OPT int_or_var OPT auto_using OPT hintbases
-| "debug" "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases
-| "info_eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases
-| "dfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases
-| "bfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases
+| "auto" OPT nat_or_var OPT auto_using OPT hintbases
+| "info_auto" OPT nat_or_var OPT auto_using OPT hintbases
+| "debug" "auto" OPT nat_or_var OPT auto_using OPT hintbases
+| "eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases
+| "new" "auto" OPT nat_or_var OPT auto_using OPT hintbases
+| "debug" "eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases
+| "info_eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases
+| "dfs" "eauto" OPT nat_or_var OPT auto_using OPT hintbases
+| "bfs" "eauto" OPT nat_or_var OPT auto_using OPT hintbases
 | "autounfold" OPT hintbases OPT clause_dft_concl
 | "autounfold_one" OPT hintbases OPT ( "in" ident )
 | "unify" one_term one_term OPT ( "with" ident )
 | "convert_concl_no_check" one_term
-| "typeclasses" "eauto" OPT "bfs" OPT int_or_var OPT ( "with" LIST1 ident )
+| "typeclasses" "eauto" OPT "bfs" OPT nat_or_var OPT ( "with" LIST1 ident )
 | "head_of_constr" ident one_term
 | "not_evar" one_term
 | "is_ground" one_term
@@ -1859,7 +1862,7 @@ simple_tactic: [
 | "functional" "inversion" [ ident | natural ] OPT qualid      (* funind plugin *)
 | "functional" "induction" term OPT ( "using" one_term OPT ( "with" bindings ) ) OPT ( "as" simple_intropattern )      (* funind plugin *)
 | "soft" "functional" "induction" LIST1 one_term OPT ( "using" one_term OPT ( "with" bindings ) ) OPT ( "as" simple_intropattern )      (* funind plugin *)
-| "psatz_Z" OPT int_or_var ltac_expr
+| "psatz_Z" OPT nat_or_var ltac_expr
 | "xlia" ltac_expr      (* micromega plugin *)
 | "xnlia" ltac_expr      (* micromega plugin *)
 | "xnra" ltac_expr      (* micromega plugin *)
@@ -1869,8 +1872,8 @@ simple_tactic: [
 | "sos_R" ltac_expr      (* micromega plugin *)
 | "lra_Q" ltac_expr      (* micromega plugin *)
 | "lra_R" ltac_expr      (* micromega plugin *)
-| "psatz_R" OPT int_or_var ltac_expr
-| "psatz_Q" OPT int_or_var ltac_expr
+| "psatz_R" OPT nat_or_var ltac_expr
+| "psatz_Q" OPT nat_or_var ltac_expr
 | "zify_iter_specs"      (* micromega plugin *)
 | "zify_op"      (* micromega plugin *)
 | "zify_saturate"      (* micromega plugin *)
@@ -1942,7 +1945,7 @@ simple_tactic: [
 | "field_simplify_eq" OPT ( "[" LIST1 one_term "]" ) OPT ( "in" ident )
 | "intuition" OPT ltac_expr
 | "nsatz" OPT ( "with" "radicalmax" ":=" one_term "strategy" ":=" one_term "parameters" ":=" one_term "variables" ":=" one_term )
-| "psatz" one_term OPT int_or_var
+| "psatz" one_term OPT nat_or_var
 | "ring" OPT ( "[" LIST1 one_term "]" )
 | "ring_simplify" OPT ( "[" LIST1 one_term "]" ) LIST1 one_term OPT ( "in" ident )
 | "match" ltac2_expr5 "with" OPT ltac2_branches "end"
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 70be55f843..a953ca8898 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -37,6 +37,9 @@ let wit_pre_ident : string uniform_genarg_type =
 let wit_int_or_var =
   make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var"
 
+let wit_nat_or_var =
+  make0 ~dyn:(val_tag (topwit wit_nat)) "nat_or_var"
+
 let wit_ident =
   make0 "ident"
 
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index bd34af5543..0a8fdf53b1 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -35,6 +35,8 @@ val wit_pre_ident : string uniform_genarg_type
 
 val wit_int_or_var : (int or_var, int or_var, int) genarg_type
 
+val wit_nat_or_var : (int or_var, int or_var, int) genarg_type
+
 val wit_ident : Id.t uniform_genarg_type
 
 val wit_hyp : (lident, lident, Id.t) genarg_type
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index b7ac71181a..e39c066c95 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -122,10 +122,10 @@ END
 
 TACTIC EXTEND constructor
 | [ "constructor" ] -> { Tactics.any_constructor false None }
-| [ "constructor" int_or_var(i) ] -> {
+| [ "constructor" nat_or_var(i) ] -> {
     Tactics.constructor_tac false None i NoBindings
   }
-| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> {
+| [ "constructor" nat_or_var(i) "with" bindings(bl) ] -> {
     let tac bl = Tactics.constructor_tac false None i bl in
     Tacticals.New.tclDELAYEDWITHHOLES false bl tac
   }
@@ -133,10 +133,10 @@ END
 
 TACTIC EXTEND econstructor
 | [ "econstructor" ] -> { Tactics.any_constructor true None }
-| [ "econstructor" int_or_var(i) ] -> {
+| [ "econstructor" nat_or_var(i) ] -> {
     Tactics.constructor_tac true None i NoBindings
   }
-| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> {
+| [ "econstructor" nat_or_var(i) "with" bindings(bl) ] -> {
     let tac bl = Tactics.constructor_tac true None i bl in
     Tacticals.New.tclDELAYEDWITHHOLES true bl tac
   }
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index a2a47c0bf4..6ab82b1253 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -686,7 +686,7 @@ let hResolve_auto id c t =
 }
 
 TACTIC EXTEND hresolve_core
-| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" int_or_var(occ) "in" constr(t) ] -> { hResolve id c occ t }
+| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" nat_or_var(occ) "in" constr(t) ] -> { hResolve id c occ t }
 | [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "in" constr(t) ] -> { hResolve_auto id c t }
 END
 
@@ -695,7 +695,7 @@ END
 *)
 
 TACTIC EXTEND hget_evar
-| [ "hget_evar" int_or_var(n) ] -> { Evar_tactics.hget_evar n }
+| [ "hget_evar" nat_or_var(n) ] -> { Evar_tactics.hget_evar n }
 END
 
 (**********************************************************************)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 7e8400910c..eed9419946 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -96,17 +96,17 @@ TACTIC EXTEND debug_trivial
 END
 
 TACTIC EXTEND auto
-| [ "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
+| [ "auto" nat_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
     { Auto.h_auto n (eval_uconstrs ist lems) db }
 END
 
 TACTIC EXTEND info_auto
-| [ "info_auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
+| [ "info_auto" nat_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
     { Auto.h_auto ~debug:Info n (eval_uconstrs ist lems) db }
 END
 
 TACTIC EXTEND debug_auto
-| [ "debug" "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
+| [ "debug" "auto" nat_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
     { Auto.h_auto ~debug:Debug n (eval_uconstrs ist lems) db }
 END
 
@@ -130,15 +130,15 @@ let deprecated_bfs tacname =
 }
 
 TACTIC EXTEND eauto
-| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
+| [ "eauto" nat_or_var_opt(n) nat_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
     {
       ( match n,p with Some _, Some _ -> deprecated_eauto_bfs () | _ -> () );
       Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
 END
 
-TACTIC EXTEND new_eauto
-| [ "new" "auto" int_or_var_opt(n) auto_using(lems)
+TACTIC EXTEND new_eauto (* todo: name doesn't match syntax *)
+| [ "new" "auto" nat_or_var_opt(n) auto_using(lems)
     hintbases(db) ] ->
     { match db with
       | None -> Auto.new_full_auto (make_depth n) (eval_uconstrs ist lems)
@@ -146,7 +146,7 @@ TACTIC EXTEND new_eauto
 END
 
 TACTIC EXTEND debug_eauto
-| [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
+| [ "debug" "eauto" nat_or_var_opt(n) nat_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
     {
       ( match n,p with Some _, Some _ -> (deprecated_bfs "debug eauto") () | _ -> () );
@@ -154,7 +154,7 @@ TACTIC EXTEND debug_eauto
 END
 
 TACTIC EXTEND info_eauto
-| [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
+| [ "info_eauto" nat_or_var_opt(n) nat_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
     {
       ( match n,p with Some _, Some _ -> (deprecated_bfs "info_eauto") () | _ -> () );
@@ -162,13 +162,13 @@ TACTIC EXTEND info_eauto
 END
 
 TACTIC EXTEND dfs_eauto
-| [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems)
+| [ "dfs" "eauto" nat_or_var_opt(p) auto_using(lems)
       hintbases(db) ] ->
     { Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db }
 END
 
 TACTIC EXTEND bfs_eauto
-| [ "bfs" "eauto" int_or_var_opt(p) auto_using(lems)
+| [ "bfs" "eauto" nat_or_var_opt(p) auto_using(lems)
       hintbases(db) ] ->
     { Eauto.gen_eauto (true, Eauto.make_depth p) (eval_uconstrs ist lems) db }
 END
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 8c2e633be5..0f59ac07b4 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -86,13 +86,13 @@ END
 
 (** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *)
 TACTIC EXTEND typeclasses_eauto
- | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
+ | [ "typeclasses" "eauto" "bfs" nat_or_var_opt(d) "with" ne_preident_list(l) ] ->
     { typeclasses_eauto ~depth:d ~strategy:Bfs l }
- | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
+ | [ "typeclasses" "eauto" nat_or_var_opt(d) "with" ne_preident_list(l) ] ->
     { typeclasses_eauto ~depth:d l }
- | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) ] -> {
+ | [ "typeclasses" "eauto" "bfs" nat_or_var_opt(d) ] -> {
      typeclasses_eauto ~depth:d ~strategy:Bfs ~only_classes:true [Class_tactics.typeclasses_db] }
- | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> {
+ | [ "typeclasses" "eauto" nat_or_var_opt(d) ] -> {
      typeclasses_eauto ~depth:d ~only_classes:true [Class_tactics.typeclasses_db] }
 END
 
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index c2e95c45f9..b1b96ea9a7 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -112,8 +112,8 @@ GRAMMAR EXTEND Gram
           | true  , None -> TacThens (ta0,first) } ]
     | "3" RIGHTA
       [ IDENT "try"; ta = ltac_expr -> { TacTry ta }
-      | IDENT "do"; n = int_or_var; ta = ltac_expr -> { TacDo (n,ta) }
-      | IDENT "timeout"; n = int_or_var; ta = ltac_expr -> { TacTimeout (n,ta) }
+      | IDENT "do"; n = nat_or_var; ta = ltac_expr -> { TacDo (n,ta) }
+      | IDENT "timeout"; n = nat_or_var; ta = ltac_expr -> { TacTimeout (n,ta) }
       | IDENT "time"; s = OPT string; ta = ltac_expr -> { TacTime (s,ta) }
       | IDENT "repeat"; ta = ltac_expr -> { TacRepeat ta }
       | IDENT "progress"; ta = ltac_expr -> { TacProgress ta }
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 89a14c7c12..43957bbde5 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -190,7 +190,7 @@ open Pvernac.Vernac_
 
 GRAMMAR EXTEND Gram
   GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
-  bindings red_expr int_or_var open_constr uconstr
+  bindings red_expr int_or_var nat_or_var open_constr uconstr
   simple_intropattern in_clause clause_dft_concl hypident destruction_arg;
 
   int_or_var:
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 94e398fe5d..196a68e67c 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -29,6 +29,7 @@ let quantified_hypothesis =
   Entry.create "quantified_hypothesis"
 let destruction_arg = Entry.create "destruction_arg"
 let int_or_var = Entry.create "int_or_var"
+let nat_or_var = Entry.create "nat_or_var"
 let simple_intropattern =
   Entry.create "simple_intropattern"
 let in_clause = Entry.create "in_clause"
@@ -52,6 +53,7 @@ let () =
   let open Stdarg in
   let open Tacarg in
   register_grammar wit_int_or_var (int_or_var);
+  register_grammar wit_nat_or_var (nat_or_var);
   register_grammar wit_intro_pattern (simple_intropattern); (* To remove at end of deprecation phase *)
 (* register_grammar wit_intropattern (intropattern); *) (* To be added at end of deprecation phase *)
   register_grammar wit_simple_intropattern (simple_intropattern);
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 3a4a081c93..c0bf6b9f76 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -27,6 +27,7 @@ val uconstr : constr_expr Entry.t
 val quantified_hypothesis : quantified_hypothesis Entry.t
 val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Entry.t
 val int_or_var : int Locus.or_var Entry.t
+val nat_or_var : int Locus.or_var Entry.t
 val simple_tactic : raw_tactic_expr Entry.t
 val simple_intropattern : constr_expr intro_pattern_expr CAst.t Entry.t
 val in_clause : Names.lident Locus.clause_expr Entry.t
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 871f418915..8bee7afa2c 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -799,6 +799,7 @@ let intern_ltac ist tac =
 
 let () =
   Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var);
+  Genintern.register_intern0 wit_nat_or_var (lift intern_int_or_var);
   Genintern.register_intern0 wit_smart_global (lift intern_smart_global);
   Genintern.register_intern0 wit_ref (lift intern_global_reference);
   Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c));
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index db86567114..00ac155f0e 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2099,6 +2099,7 @@ let interp_pre_ident ist env sigma s =
 
 let () =
   register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
+  register_interp0 wit_nat_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
   register_interp0 wit_smart_global (lift interp_reference);
   register_interp0 wit_ref (lift interp_reference);
   register_interp0 wit_pre_ident (lift interp_pre_ident);
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 5f09666778..90546ea939 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -279,6 +279,7 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) =
 
 let () =
   Genintern.register_subst0 wit_int_or_var (fun _ v -> v);
+  Genintern.register_subst0 wit_nat_or_var (fun _ v -> v);
   Genintern.register_subst0 wit_ref subst_global_reference;
   Genintern.register_subst0 wit_smart_global subst_global_reference;
   Genintern.register_subst0 wit_pre_ident (fun _ v -> v);
diff --git a/plugins/micromega/g_micromega.mlg b/plugins/micromega/g_micromega.mlg
index 40eea91b31..852a485329 100644
--- a/plugins/micromega/g_micromega.mlg
+++ b/plugins/micromega/g_micromega.mlg
@@ -29,7 +29,7 @@ open Tacarg
 DECLARE PLUGIN "micromega_plugin"
 
 TACTIC EXTEND PsatzZ
-| [ "psatz_Z" int_or_var(i) tactic(t) ] -> {  (Coq_micromega.psatz_Z i
+| [ "psatz_Z" nat_or_var(i) tactic(t) ] -> {  (Coq_micromega.psatz_Z i
                                                (Tacinterp.tactic_of_value ist t))
                                                }
 | [ "psatz_Z" tactic(t)] -> {  (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) }
@@ -74,12 +74,12 @@ TACTIC EXTEND LRA_R
 END
 
 TACTIC EXTEND PsatzR
-| [ "psatz_R" int_or_var(i) tactic(t) ] -> {   (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) }
+| [ "psatz_R" nat_or_var(i) tactic(t) ] -> {   (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) }
 | [ "psatz_R" tactic(t) ] -> {   (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) }
 END
 
 TACTIC EXTEND PsatzQ
-| [ "psatz_Q" int_or_var(i) tactic(t) ] -> {  (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) }
+| [ "psatz_Q" nat_or_var(i) tactic(t) ] -> {  (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) }
 | [ "psatz_Q" tactic(t) ] -> {  (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) }
 END
 
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index ccdf5fa68e..f06b460ee9 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -1792,7 +1792,7 @@ GRAMMAR EXTEND Gram
       { ssrdotac_expr ~loc noindex m tac clauses }
     | IDENT "do"; tac = ssrortacarg; clauses = ssrclauses ->
       { ssrdotac_expr ~loc noindex Once tac clauses }
-    | IDENT "do"; n = int_or_var; m = ssrmmod;
+    | IDENT "do"; n = nat_or_var; m = ssrmmod;
                   tac = ssrdotac; clauses = ssrclauses ->
       { ssrdotac_expr ~loc (mk_index ~loc n) m tac clauses }
     ] ];