# HG changeset patch
# User wenzelm
# Date 1128948225 -7200
# Node ID 38c889d77282b467414ab39fd247954e94a2bfe0
# Parent  405fb812e7387cb11db66f9ad4b2f483cb052612
updated print_tac;

diff -r 405fb812e738 -r 38c889d77282 doc-src/Ref/tactic.tex
--- a/doc-src/Ref/tactic.tex	Mon Oct 10 05:46:17 2005 +0200
+++ b/doc-src/Ref/tactic.tex	Mon Oct 10 14:43:45 2005 +0200
@@ -634,7 +634,7 @@
 \index{tracing!of tactics}
 \begin{ttbox} 
 pause_tac: tactic
-print_tac: tactic
+print_tac: string -> tactic
 \end{ttbox}
 These tactics print tracing information when they are applied to a proof
 state.  Their output may be difficult to interpret.  Note that certain of
@@ -646,7 +646,7 @@
 from the terminal.  If this line is blank then it returns the proof state
 unchanged; otherwise it fails (which may terminate a repetition).
 
-\item[\ttindexbold{print_tac}] 
+\item[\ttindexbold{print_tac}~$msg$] 
 returns the proof state unchanged, with the side effect of printing it at
 the terminal.
 \end{ttdescription}