aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/changelog/04-tactics/13381-bfs_eauto.rst4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/changelog/04-tactics/13381-bfs_eauto.rst b/doc/changelog/04-tactics/13381-bfs_eauto.rst
index a2c5e44340..a51f96d0a2 100644
--- a/doc/changelog/04-tactics/13381-bfs_eauto.rst
+++ b/doc/changelog/04-tactics/13381-bfs_eauto.rst
@@ -1,6 +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";
+ 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).