Added a note about the ambiguity of the syntax "qualid" in "tacarg"

(see coq-club message from 3 Jan 2008).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10422 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 0 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 48d27a50a2..af9241e9dc 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -59,6 +59,14 @@ Figure~\ref{ltactop}.
 \item The infix tacticals ``\dots\ {\tt ||} \dots'' and ``\dots\ {\tt
     ;} \dots'' are associative. 
 
+\item In {\tacarg}, there is an overlap between {\qualid} as a
+direct tactic argument and {\qualid} as a particular case of
+{\term}. The resolution is done by first looking for a reference of
+the tactic language and if it fails, for a reference to a term. To
+force the resolution as a reference of the tactic language, use the
+form {\tt ltac :} {\qualid}. To force the resolution as a reference to
+a term, use the syntax {\tt ({\qualid})}.
+
 \item As shown by the figure, tactical {\tt ||} binds more than the
 prefix tacticals {\tt try}, {\tt repeat}, {\tt do}, {\tt info} and
 {\tt abstract} which themselves bind more than the postfix tactical