Skip to content

Commit

Permalink
Adding change log for #18576
Browse files Browse the repository at this point in the history
  • Loading branch information
herbelin committed Jan 30, 2024
1 parent c728193 commit a90fcef
Showing 1 changed file with 7 additions and 0 deletions.
@@ -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 <https://github.com/coq/coq/pull/18576>`_,
fixes `#4056 <https://github.com/coq/coq/issues/4056>`_,
by Hugo Herbelin).

0 comments on commit a90fcef

Please sign in to comment.