diff options
Diffstat (limited to 'doc/refman/RefMan-tacex.tex')
| -rw-r--r-- | doc/refman/RefMan-tacex.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex index dbd863469..9af44115a 100644 --- a/doc/refman/RefMan-tacex.tex +++ b/doc/refman/RefMan-tacex.tex @@ -1084,7 +1084,7 @@ is undecidable in general case, don't expect miracles from it! % \SeeAlso file \texttt{theories/DEMOS/DemoQuote.v} -\SeeAlso comments of source file \texttt{tactics/contrib/polynom/quote.ml} +\SeeAlso comments of source file \texttt{plugins/quote/quote.ml} \SeeAlso the \texttt{ring} tactic (Chapter~\ref{ring}) |