Documentation: a simple example for [numgoals].

Now that [idtac] can print a single message for several goals, printing the number of goals is readable.

1 files changed, 9 insertions, 11 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 49b0cadf0..13ff9afb1 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -914,17 +914,15 @@ The number of goals under focus can be recovered using the {\tt
   numgoals} function. Combined with the {\tt guard} command below, it
 can be used to branch over the number of goals produced by previous tactics.
 
-%% spiwack: could be a reasonable example, but unfortunately it turns out
-%% to be more confusing than anything.
-%% \begin{coq_example*}
-%% Ltac pr_numgoals := let n := numgoals in idtac n.
-
-%% Goal True /\ True /\ True.
-%% split;[|split].
-%% \end{coq_example*}
-%% \begin{coq_example}
-%% all:pr_numgoals.
-%% \end{coq_example}
+\begin{coq_example*}
+Ltac pr_numgoals := let n := numgoals in idtac "There are" n "goals".
+
+Goal True /\ True /\ True.
+split;[|split].
+\end{coq_example*}
+\begin{coq_example}
+all:pr_numgoals.
+\end{coq_example}
 
 \subsubsection[Testing boolean expressions]{Testing boolean expressions\index{Ltac!guard}\index{guard!in Ltac}}