diff options
Diffstat (limited to 'doc/refman/RefMan-com.tex')
| -rw-r--r-- | doc/refman/RefMan-com.tex | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 45230fb6e5..9790111f14 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -2,6 +2,7 @@ \ttindex{coqtop} \ttindex{coqc} \ttindex{coqchk}} +%HEVEA\cutname{commands.html} There are three \Coq~commands: \begin{itemize} |