Merge PR #10215: Refine typing of vernacular commands

Reviewed-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares

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.