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 | 7 |
1 files changed, 7 insertions, 0 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 53828db951..12d458a72c 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 @@ -3,3 +3,10 @@ :ref:`advanced-recursive-functions` of 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 + inside a module type. In order to declare a module type parameter that + happens to be a morphism, use ``Parameter Morphism``. See + :ref:`deprecated_syntax_for_generalized_rewriting` for the updated + documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, + by Enrico Tassi). |