diff options
| author | Enrico Tassi | 2019-05-22 17:50:44 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 13:58:43 +0200 |
| commit | 2ebd73901edb94030aa804572cbe86d486ca6732 (patch) | |
| tree | 0cba6dcfaac70fc01f622d06ad9442570f823319 /doc/changelog | |
| parent | 0f1814bcbaafbd93d7c7587eef8826a80b65477f (diff) | |
[rewrite] Add Morphism syntax made different for module type parameters
Diffstat (limited to 'doc/changelog')
| -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). |