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

Reviewed-by: Zimmi48

8 files changed, 96 insertions, 82 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"