Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"

Reviewed-by: Zimmi48

5 files changed, 35 insertions, 3 deletions

diff --git a/doc/changelog/04-tactics/13381-bfs_eauto.rst b/doc/changelog/04-tactics/13381-bfs_eauto.rst
new file mode 100644
index 0000000000..a51f96d0a2
--- /dev/null
+++ b/doc/changelog/04-tactics/13381-bfs_eauto.rst
@@ -0,0 +1,6 @@
+- **Deprecated:**
+  Undocumented :n:`eauto @int_or_var @int_or_var` syntax in favor of new ``bfs eauto``.
+  Also deprecated 2-integer syntax for ``debug eauto`` and ``info_eauto``;
+  replacement TBD.
+  (`#13381 <https://github.com/coq/coq/pull/13381>`_,
+  by Jim Fehrle).
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index a787d769fb..033ece04de 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1623,6 +1623,7 @@ simple_tactic: [
 | "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
 | "autounfold" hintbases clause_dft_concl
 | "autounfold_one" hintbases "in" hyp
 | "autounfold_one" hintbases
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 26474d950a..e6fc6188b7 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1754,6 +1754,7 @@ simple_tactic: [
 | "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
 | "autounfold" OPT hintbases OPT clause_dft_concl
 | "autounfold_one" OPT hintbases OPT ( "in" ident )
 | "unify" one_term one_term OPT ( "with" ident )
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 15861d49be..7e8400910c 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -116,12 +116,25 @@ END
 
 let make_depth n = snd (Eauto.make_dimension n None)
 
+(* deprecated in 8.13; the second int_or_var will be removed *)
+let deprecated_eauto_bfs =
+  CWarnings.create
+    ~name:"eauto_bfs" ~category:"deprecated"
+    (fun () -> Pp.str "The syntax [eauto @int_or_var @int_or_var] is deprecated. Use [bfs eauto] instead.")
+
+let deprecated_bfs tacname =
+  CWarnings.create
+    ~name:"eauto_bfs" ~category:"deprecated"
+    (fun () -> Pp.str "The syntax [" ++ Pp.str tacname ++ Pp.str "@int_or_var @int_or_var] is deprecated. No replacement yet.")
+
 }
 
 TACTIC EXTEND eauto
 | [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    { Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) 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
@@ -135,13 +148,17 @@ END
 TACTIC EXTEND debug_eauto
 | [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    { Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
+    {
+      ( match n,p with Some _, Some _ -> (deprecated_bfs "debug eauto") () | _ -> () );
+      Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
 END
 
 TACTIC EXTEND info_eauto
 | [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    { Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
+    {
+      ( match n,p with Some _, Some _ -> (deprecated_bfs "info_eauto") () | _ -> () );
+      Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
 END
 
 TACTIC EXTEND dfs_eauto
@@ -150,6 +167,12 @@ TACTIC EXTEND dfs_eauto
     { 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)
+      hintbases(db) ] ->
+    { Eauto.gen_eauto (true, Eauto.make_depth p) (eval_uconstrs ist lems) db }
+END
+
 TACTIC EXTEND autounfold
 | [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> { Eauto.autounfold_tac db cl }
 END
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 5fb038a767..f40bbc813e 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -30,4 +30,5 @@ val autounfold : hint_db_name list -> Locus.clause -> unit Proofview.tactic
 val autounfold_tac : hint_db_name list option -> Locus.clause -> unit Proofview.tactic
 val autounfold_one : hint_db_name list -> Locus.hyp_location option -> unit Proofview.tactic
 
+val make_depth : int option -> int
 val make_dimension : int option -> int option -> bool * int