From 4131b14ac8ea93b54583c0c6fc0dff310a9c5172 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 28 May 2019 22:20:03 +0200 Subject: Fix typo in changelog --- .../02-specification-language/10215-rm-maybe-open-proof.rst | 5 ++--- 1 file 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 `_, + annotation, see :ref:`advanced-recursive-functions` for the updated + documentation (`#10215 `_, by Enrico Tassi). - The legacy command Add Morphism always opens a proof and cannot be used -- cgit v1.2.3