diff options
| author | Hugo Herbelin | 2020-04-21 10:56:13 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-21 10:56:13 +0200 |
| commit | 99c1a97da611210cc8322780c903875a9201929e (patch) | |
| tree | c5ad5ec09153b4c39387aac4d71bae37045f0612 /doc | |
| parent | c30594f55750996398eb3947838eaf1f906f08c9 (diff) | |
| parent | b5cb67b877ca39053ccd522487a9bffc7736cf3b (diff) | |
Merge PR #11883: Fix #7812: autounfold's behavior depends on file names
Reviewed-by: herbelin
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). |