diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-23 15:41:02 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-23 15:41:02 +0000 |
| commit | 492b5280384263a5dc9f5fb60c9c8d6bcbc8afce (patch) | |
| tree | 8f7235c2e72650c5af39f88bf8ed18eece8bf417 | |
| parent | 287058532aefd848df5d83ee29707359672b626f (diff) | |
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
| -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} |