From 9460bde3509f8e0cc98c32401242f4e9154ac75d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 20 Dec 2003 10:52:14 +0000
Subject: Typo

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8432 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-tac.tex   | 2 +-
 doc/RefMan-tacex.tex | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 3605ebff79..52419e6bf0 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -1160,7 +1160,7 @@ last introduced hypothesis.
 \end{Variants}
 
 \subsection{\tt intros {\intropattern} {\ldots} {\intropattern}}
-\label{intros-patterns}
+\label{intros-pattern}
 \tacindex{intros \intropattern}
 
 The tactic {\tt intros} applied to introduction patterns performs both
diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex
index f82416869d..eb5f873182 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}
-- 
cgit v1.2.3