diff options
Diffstat (limited to 'doc/refman/RefMan-int.tex')
-rw-r--r-- | doc/refman/RefMan-int.tex | 2 |
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 |