aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/04-tactics/13381-bfs_eauto.rst
diff options
context:
space:
mode:
Diffstat (limited to 'doc/changelog/04-tactics/13381-bfs_eauto.rst')
-rw-r--r--doc/changelog/04-tactics/13381-bfs_eauto.rst6
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/changelog/04-tactics/13381-bfs_eauto.rst b/doc/changelog/04-tactics/13381-bfs_eauto.rst
index f37fbfe52b..e63241e46c 100644
--- a/doc/changelog/04-tactics/13381-bfs_eauto.rst
+++ b/doc/changelog/04-tactics/13381-bfs_eauto.rst
@@ -1,6 +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``.
- (Use ``bfs eauto`` with the :flag:`Info Eauto` or :flag:`Debug Eauto` flags instead.)
+ Undocumented :n:`eauto @nat_or_var @nat_or_var` syntax in favor of new :tacn:`bfs eauto`.
+ Also deprecated 2-integer syntax for :tacn:`debug eauto` and :tacn:`info_eauto`.
+ (Use :tacn:`bfs eauto` with the :flag:`Info Eauto` or :flag:`Debug Eauto` flags instead.)
(`#13381 <https://github.com/coq/coq/pull/13381>`_,
by Jim Fehrle).