aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-com.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman/RefMan-com.tex')
-rw-r--r--doc/refman/RefMan-com.tex3
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index a93733256..49bcdb1db 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -1,6 +1,7 @@
\chapter[The \Coq~commands]{The \Coq~commands\label{Addoc-coqc}
\ttindex{coqtop}
-\ttindex{coqc}}
+\ttindex{coqc}
+\ttindex{coqchk}}
There are three \Coq~commands:
\begin{itemize}