doc/changelog/08-cli-tools/13624-master+fix13581-extraction-letin-in-ind-arity.rst


1
2
3
4
5
6

- **Fixed:**
  Failure of extraction in the presence of inductive types with local
  definitions in parameters
  (`#13624 <https://github.com/coq/coq/pull/13624>`_,
  fixes `#13581 <https://github.com/coq/coq/issues/13581>`_,
  by Hugo Herbelin).