Merge PR #10215: Refine typing of vernacular commands

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

4 files changed, 25 insertions, 8 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
new file mode 100644
index 0000000000..21ec7f8e5b
--- /dev/null
+++ b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst
@@ -0,0 +1,11 @@
+- Function always opens a proof when used with a ``measure`` or ``wf``
+  annotation, see :ref:`advanced-recursive-functions` for 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).
diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index 75251d8e33..300d62285a 100644
--- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -145,12 +145,11 @@ END
   it gives an error message that is basically impossible to understand. *)
 
 VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
-| ![ proof ] [ "Cmd9" ] ->
+| ![ proof_query ] [ "Cmd9" ] ->
   { fun ~pstate ->
-    Option.iter (fun (pstate : Proof_global.t) ->
-        let sigma, env = Pfedit.get_current_context pstate in
-        let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in
-        Feedback.msg_notice
-          (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)) pstate;
-    pstate }
+    let sigma, env = Pfedit.get_current_context pstate in
+    let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in
+    Feedback.msg_notice
+      (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
+  }
 END
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.
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 8c5ad785e4..c93984661e 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -737,7 +737,7 @@ used by ``Function``. A more precise description is given below.
       decreases at each recursive call of :token:`term`. The order must be well-founded.
       Parameters of the function are bound in :token:`term`.
 
-   Depending on the annotation, the user is left with some proof
+   If the annotation is ``measure`` or ``fw``, the user is left with some proof
    obligations that will be used to define the function. These proofs
    are: proofs that each recursive call is actually decreasing with
    respect to the given criteria, and (if the criteria is `wf`) a proof