Use nat_or_var where negative values don't make sense

3 files changed, 73 insertions, 68 deletions

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"