aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/RefMan-tacex.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/RefMan-tacex.tex')
-rw-r--r--doc/RefMan-tacex.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex
index f82416869..eb5f87318 100644
--- a/doc/RefMan-tacex.tex
+++ b/doc/RefMan-tacex.tex
@@ -809,7 +809,7 @@ is undecidable in general case, don't expect miracles from it!
\SeeAlso comments of source file \texttt{tactics/contrib/polynom/quote.ml}
-\SeeAlso the tactic \texttt{Ring} (chapter \ref{Ring})
+\SeeAlso the tactic \texttt{ring} (chapter \ref{ring})
\section{Using the tactical language}