aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-com.tex
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-01-29 22:40:58 +0100
committerPierre-Marie Pédrot2015-01-29 22:40:58 +0100
commita340265c9f88df990649481c8ecbe8a513ac4756 (patch)
treec9e02defb10bcdb258d75cb6f156657654f65f1f /doc/refman/RefMan-com.tex
parent51b15993cb4a9cc2521b6107b7f4195b21040087 (diff)
parentdb293d185f8deb091d4b086f327caa0f376d67d7 (diff)
Merge branch 'v8.5'
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 a937332569..49bcdb1db7 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}