blob: 53828db951927122c3d26825776c05ca82a541aa (
plain)
1
2
3
4
5
|
- Function always opens a proof when used with a ``measure`` or ``wf``
annotation, see Description of the changes, with possible link to
:ref:`advanced-recursive-functions` of the updated documentation
(`#10215 <https://github.com/coq/coq/pull/10215>`_,
by Enrico Tassi).
|
