From 5f9b15657dacd258fbd9084424afd4aa96929f3f Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 5 Aug 2014 16:25:04 +0200
Subject: Documentation: a simple example for [numgoals].

Now that [idtac] can print a single message for several goals, printing the number of goals is readable.
---
 doc/refman/RefMan-ltac.tex | 20 +++++++++-----------
 1 file changed, 9 insertions(+), 11 deletions(-)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 49b0cadf05..13ff9afb1b 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}}
 
-- 
cgit v1.2.3