tactiques

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

1 files changed, 2 insertions, 2 deletions

diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex
index e8bcb3d7fa..985c60babf 100755
--- a/doc/RefMan-pro.tex
+++ b/doc/RefMan-pro.tex
@@ -144,8 +144,8 @@ as a {\tt Theorem}, the name {\ident} is known at all section levels:
 
 \subsection{\tt Proof {\term}.}\comindex{Proof}
 This command applies in proof editing mode. It is equivalent to {\tt
-  Exact {\term}; Save.} That is, you have to give the full proof in
-one gulp, as a proof term (see section \ref{Exact}).
+  exact {\term}; Save.} That is, you have to give the full proof in
+one gulp, as a proof term (see section \ref{exact}).
 
 \begin{Variants}
 \item{\tt Proof.} is a noop which is useful to delimit the sequence of