diff options
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 6 |
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} |