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

1 files changed, 2 insertions, 4 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 2fc8b48b0..3948bbe85 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}