diff options
| author | Enrico Tassi | 2019-05-28 22:20:03 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 13:58:43 +0200 |
| commit | 4131b14ac8ea93b54583c0c6fc0dff310a9c5172 (patch) | |
| tree | 21ff2bd2fb363c85b880d3aeaf460b1a9e6ceb3e | |
| parent | 9bc58fc7038d627b06c176854811d1947bca09f2 (diff) | |
Fix typo in changelog
| -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 |