From bc73bc1ef78f6cb5cabb173e633be9cc96a05180 Mon Sep 17 00:00:00 2001
From: narboux
Date: Mon, 1 Dec 2003 10:23:32 +0000
Subject: idtac parle

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8370 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-ltac.tex | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/doc/RefMan-ltac.tex b/doc/RefMan-ltac.tex
index 73731bea5a..d4408ace7e 100644
--- a/doc/RefMan-ltac.tex
+++ b/doc/RefMan-ltac.tex
@@ -352,9 +352,11 @@ tries to apply $v_2$ and so on. It fails if there is no solving tactic.\\
 
 We have the identity tactic:\\
 
-{\tt Idtac}\\
+{\tt Idtac} and {\tt Idtac ``message''}\\
 
 It leaves the goal unchanged but it appears in the proof script.
+If there is a string as an argument then it prints this string on the
+standard output. 
 
 \subsubsection{Failing}
 
-- 
cgit v1.2.3