aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-int.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman/RefMan-int.tex')
-rw-r--r--doc/refman/RefMan-int.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex
index c93d7217f..14b14ae57 100644
--- a/doc/refman/RefMan-int.tex
+++ b/doc/refman/RefMan-int.tex
@@ -48,7 +48,7 @@ commands are processed from a file.
the {\tt coqc} command from the operating system.
\end{itemize}
-These two modes are documented in chapter \ref{Addoc-coqc}.
+These two modes are documented in Chapter~\ref{Addoc-coqc}.
Other modes of interaction with \Coq{} are possible: through an emacs
shell window, an emacs generic user-interface for proof assistant