diff options
| -rw-r--r-- | doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst index 12d458a72c..21ec7f8e5b 100644 --- a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst +++ b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst @@ -1,7 +1,6 @@ - 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>`_, + annotation, see :ref:`advanced-recursive-functions` for the updated + documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, by Enrico Tassi). - The legacy command Add Morphism always opens a proof and cannot be used |