From 2ebd73901edb94030aa804572cbe86d486ca6732 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 17:50:44 +0200 Subject: [rewrite] Add Morphism syntax made different for module type parameters --- .../02-specification-language/10215-rm-maybe-open-proof.rst | 7 +++++++ doc/sphinx/addendum/generalized-rewriting.rst | 7 +++++++ 2 files changed, 14 insertions(+) (limited to 'doc') 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 `_, 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 `_, + by Enrico Tassi). diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index e58049b8d0..2ea0861e47 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -563,6 +563,7 @@ Printing relations and morphisms of morphisms, the :cmd:`Print Instances` command can be useful to understand what additional morphisms should be registered. +.. _deprecated_syntax_for_generalized_rewriting: Deprecated syntax and backward incompatibilities ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -589,6 +590,12 @@ Deprecated syntax and backward incompatibilities bi-implication in place of a simple implication. In practice, porting an old development to the new semantics is usually quite simple. +.. cmd:: Declare Morphism @ident : @ident + :name: Declare Morphism + + This commands is to be used in a module type to declare a parameter that + is a morphism. + Notice that several limitations of the old implementation have been lifted. In particular, it is now possible to declare several relations with the same carrier and several signatures for the same morphism. -- cgit v1.2.3