diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-22 00:36:51 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-22 00:36:51 +0100 |
| commit | 151286ec0c0887d212e7e85205352de4ddbf4bf2 (patch) | |
| tree | fc359fce2dbbfdc5250f9089079a8ad60cb1fbb4 /doc | |
| parent | 28d3bb3c8bddc63d038d8d55a34c928675fa9f7b (diff) | |
| parent | b087d133f7d6d091cce72190c05a9a09d5b37791 (diff) | |
Merge PR#482: [toplevel] Remove unusable option -notop
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-com.tex | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 2 |
2 files changed, 1 insertions, 7 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 diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index b475a5233..1d423f8b1 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -991,7 +991,7 @@ but library file names based on other roots can be obtained by using {\Coq} commands ({\tt coqc}, {\tt coqtop}, {\tt coqdep}, \dots) options {\tt -Q} or {\tt -R} (see Section~\ref{coqoptions}). Also, when an interactive {\Coq} session starts, a library of root {\tt Top} is -started, unless option {\tt -top} or {\tt -notop} is set (see +started, unless option {\tt -top} is set (see Section~\ref{coqoptions}). \subsection{Qualified names |