diff options
Diffstat (limited to 'doc/refman/RefMan-com.tex')
| -rw-r--r-- | doc/refman/RefMan-com.tex | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index bef0a1686..45230fb6e 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -123,12 +123,6 @@ The following command-line options are recognized by the commands {\tt valid for {\tt coqc} as the toplevel module name is inferred from the name of the output file. -\item[{\tt -notop}]\ % - - Use the empty logical path for the toplevel module name instead of {\tt - Top}. Not valid for {\tt coqc} as the toplevel module name is - inferred from the name of the output file. - \item[{\tt -exclude-dir} {\em directory}]\ % Exclude any subdirectory named {\em directory} while |