diff options
| author | Attila Gáspár | 2020-03-20 17:22:36 +0100 |
|---|---|---|
| committer | Attila Gáspár | 2020-04-11 11:19:04 +0200 |
| commit | b5cb67b877ca39053ccd522487a9bffc7736cf3b (patch) | |
| tree | 5b642c29f22e4c0dc5a8a82475a97226616847b8 /doc | |
| parent | c5c8ce135606f311834d4c0b9ac3e72be5ee4a36 (diff) | |
Fix #7812
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/04-tactics/11883-fix-autounfold.rst | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/doc/changelog/04-tactics/11883-fix-autounfold.rst b/doc/changelog/04-tactics/11883-fix-autounfold.rst new file mode 100644 index 0000000000..83ff177380 --- /dev/null +++ b/doc/changelog/04-tactics/11883-fix-autounfold.rst @@ -0,0 +1,13 @@ +- **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). |