From b087d133f7d6d091cce72190c05a9a09d5b37791 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 14 Mar 2017 21:24:53 +0100 Subject: [toplevel] Remove unusable option -notop MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Maxime points out that -notop cannot be used as the kernel requires all constants to belong into a module. Indeed: ``` $ rlwrap ./bin/coqtop -notop Coq < Definition foo := True. Toplevel input, characters 0-23: > Definition foo := True. > ^^^^^^^^^^^^^^^^^^^^^^^ Error: No session module started (use -top dir) Coq < Module M. Definition foo := True. End M. Module M is defined Coq < Locate foo. Constant If you see this, it's a bug.M.foo (shorter name to refer to it in current context is M.foo) ``` My rationale for the removal is that this kind of incomplete features are often confusing to newcomers ─ it has happened to me many times ─ as it can be seen for example in #397 . --- doc/refman/RefMan-com.tex | 6 ------ doc/refman/RefMan-ext.tex | 2 +- 2 files changed, 1 insertion(+), 7 deletions(-) (limited to 'doc') 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 -- cgit v1.2.3