Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"

3 files changed, 8 insertions, 0 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..a2c5e44340
--- /dev/null
+++ b/doc/changelog/04-tactics/13381-bfs_eauto.rst
@@ -0,0 +1,6 @@
+- **Deprecated:**
+  "eauto @int_or_var @int_or_var" in favor of new "bfs eauto".
+  Also deprecated 2-integer option 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 c697043f27..34c3665d1d 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1746,6 +1746,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 )