diff --git a/doc/changelog/04-tactics/18576-master+fix4056-refolding-simpl-cofix.rst b/doc/changelog/04-tactics/18576-master+fix4056-refolding-simpl-cofix.rst new file mode 100644 index 0000000000000..5b6c13fb40eba --- /dev/null +++ b/doc/changelog/04-tactics/18576-master+fix4056-refolding-simpl-cofix.rst @@ -0,0 +1,7 @@ +- **Fixed:** + The name of a cofixpoint globally defined with a name is now + systematically reused by :tacn:`simpl` after reduction, even when + the named cofixpoint is mutually defined or defined in a section + (`#18576 `_, + fixes `#4056 `_, + by Hugo Herbelin).