Document the possibility of declaring a Ltac name_goal.

1 files changed, 35 insertions, 0 deletions

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 590d71b5f3..24645a8cc3 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -346,11 +346,46 @@ Navigation in the proof tree
 
          Goals are just existential variables and existential variables do not
          get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`.
+         You may also wrap this in an Ltac-definition like:
+
+         .. coqtop:: in
+
+            Ltac name_goal name := refine ?[name].
 
       .. seealso:: :ref:`existential-variables`
 
       .. example::
 
+         This first example uses the Ltac definition above, and the named goals
+         only serve for documentation.
+
+         .. coqtop:: all
+
+            Goal forall n, n + 0 = n.
+            Proof.
+            induction n; [ name_goal base | name_goal step ].
+            [base]: {
+
+         .. coqtop:: all
+
+            reflexivity.
+
+         .. coqtop:: in
+
+            }
+
+         .. coqtop:: all
+
+            [step]: {
+
+         .. coqtop:: all
+
+            simpl.
+            f_equal.
+            assumption.
+            }
+            Qed.
+
          This can also be a way of focusing on a shelved goal, for instance:
 
          .. coqtop:: all