aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/04-tactics/11883-fix-autounfold.rst
diff options
context:
space:
mode:
Diffstat (limited to 'doc/changelog/04-tactics/11883-fix-autounfold.rst')
-rw-r--r--doc/changelog/04-tactics/11883-fix-autounfold.rst13
1 files changed, 0 insertions, 13 deletions
diff --git a/doc/changelog/04-tactics/11883-fix-autounfold.rst b/doc/changelog/04-tactics/11883-fix-autounfold.rst
deleted file mode 100644
index 83ff177380..0000000000
--- a/doc/changelog/04-tactics/11883-fix-autounfold.rst
+++ /dev/null
@@ -1,13 +0,0 @@
-- **Fixed:**
- The behavior of :tacn:`autounfold` no longer depends on the names of terms and modules
- (`#11883 <https://github.com/coq/coq/pull/11883>`_,
- fixes `#7812 <https://github.com/coq/coq/issues/7812>`_,
- by Attila Gáspár).
-- **Changed:**
- `at` clauses can no longer be used with :tacn:`autounfold`. Since they had no effect, it is safe to remove them
- (`#11883 <https://github.com/coq/coq/pull/11883>`_,
- by Attila Gáspár).
-- **Changed:**
- :tacn:`autounfold` no longer fails when the :cmd:`Opaque` command is used on constants in the hint databases
- (`#11883 <https://github.com/coq/coq/pull/11883>`_,
- by Attila Gáspár).