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

Reviewed-by: Zimmi48

11 files changed, 29 insertions, 23 deletions

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);