From 7758ceb4002d56325d2571e18e0fcaae75d0acad Mon Sep 17 00:00:00 2001
From: glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 30 Mar 2009 15:22:29 +0000
Subject: Document new quote construction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12039 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-tacex.tex | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

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}
-- 
cgit v1.2.3