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/sphinx | |
| parent | 0f1814bcbaafbd93d7c7587eef8826a80b65477f (diff) | |
[rewrite] Add Morphism syntax made different for module type parameters
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 7 |
1 files changed, 7 insertions, 0 deletions
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. |