diff options
Diffstat (limited to 'doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst')
| -rw-r--r-- | doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst | 13 |
1 files changed, 0 insertions, 13 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 deleted file mode 100644 index c201b482e5..0000000000 --- a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst +++ /dev/null @@ -1,13 +0,0 @@ -- **Changed:** - :cmd:`Function` always opens a proof when used with a ``measure`` or ``wf`` - annotation, see :ref:`advanced-recursive-functions` for the updated - documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, - by Enrico Tassi). - -- **Changed:** - The legacy command :cmd:`Add Morphism` always opens a proof and cannot be used - inside a module type. In order to declare a module type parameter that - happens to be a morphism, use :cmd:`Declare Morphism`. See - :ref:`deprecated_syntax_for_generalized_rewriting` for the updated - documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, - by Enrico Tassi). |