From 492b5280384263a5dc9f5fb60c9c8d6bcbc8afce Mon Sep 17 00:00:00 2001
From: glondu
Date: Wed, 23 Sep 2009 15:41:02 +0000
Subject: Ltac doc: only variables are accepted as message_token

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

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 2fc8b48b0b..3948bbe855 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -145,7 +145,7 @@ is understood as
 & | & {\integer}\\
 & | & {\tt (} {\tacexpr} {\tt )}\\
 \\
-{\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\term} ~|~ {\integer} \\
+{\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\ident} ~|~ {\integer} \\
 \end{tabular}
 \end{centerframe}
 \caption{Syntax of the tactic language}
@@ -416,9 +416,7 @@ unchanged but it appears in the proof script.
 \variant {\tt idtac \nelist{\messagetoken}{}}
 
 This prints the given tokens. Strings and integers are printed
-literally. If a term is given, it is printed, its variables being
-interpreted in the current environment. In particular, if a variable
-is given, its value is printed.
+literally. If a (term) variable is given, its contents are printed.
 
 
 \subsubsection[Failing]{Failing\tacindex{fail}
-- 
cgit v1.2.3