Document new quote construction

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

1 files changed, 15 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 9af44115a..306e52ebd 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -1082,6 +1082,21 @@ Undo.
 \Warning Since function inversion
 is undecidable in general case, don't expect miracles from it!
 
+\begin{Variants}
+
+\item {\tt quote {\ident} in {\term} using {\tac}}
+
+  \tac\ must be a functional tactic (starting with {\tt fun x =>})
+  and will be called with the quoted version of \term\ according to
+  \ident.
+
+\item {\tt quote {\ident} [ \ident$_1$ \dots\ \ident$_n$ ] in {\term} using {\tac}}
+
+  Same as above, but will use \ident$_1$, \dots, \ident$_n$ to
+  chose which subterms are constants (see above).
+
+\end{Variants}
+
 % \SeeAlso file \texttt{theories/DEMOS/DemoQuote.v}
 
 \SeeAlso comments of source file \texttt{plugins/quote/quote.ml}