diff options
| -rw-r--r-- | doc/refman/RefMan-com.tex | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 8 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
5 files changed, 5 insertions, 14 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 diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e4b3fcbf1..2312f891c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -71,7 +71,7 @@ module NamedDecl = Context.Named.Declaration - [env] : the underlying environment (cf Environ) - [modpath] : the current module name - [modvariant] : - * NONE before coqtop initialization (or when -notop is used) + * NONE before coqtop initialization * LIBRARY at toplevel of a compilation or a regular coqtop session * STRUCT (params,oldsenv) : inside a local module, with module parameters [params] and earlier environment [oldsenv] diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index cc1c44fe3..c9a1f0def 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -122,11 +122,10 @@ let engage () = let set_batch_mode () = batch_mode := true let toplevel_default_name = DirPath.make [Id.of_string "Top"] -let toplevel_name = ref (Some toplevel_default_name) +let toplevel_name = ref toplevel_default_name let set_toplevel_name dir = if DirPath.is_empty dir then error "Need a non empty toplevel module name"; - toplevel_name := Some dir -let unset_toplevel_name () = toplevel_name := None + toplevel_name := dir let remove_top_ml () = Mltop.remove () @@ -556,7 +555,6 @@ let parse_args arglist = if Coq_config.no_native_compiler then warning "Native compilation was disabled at configure time." else native_compiler := true - |"-notop" -> unset_toplevel_name () |"-output-context" -> output_context := true |"-profile-ltac" -> Flags.profile_ltac := true |"-q" -> no_load_rc () @@ -628,7 +626,7 @@ let init_toplevel arglist = engage (); if (not !batch_mode || List.is_empty !compile_list) && Global.env_is_initial () - then Option.iter Declaremods.start_library !toplevel_name; + then Declaremods.start_library !toplevel_name; init_library_roots (); load_vernac_obj (); require (); diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 38ceacf5e..66f782ffb 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -30,7 +30,6 @@ let print_usage_channel co command = \n -R dir coqdir recursively map physical dir to logical coqdir\ \n -Q dir coqdir map physical dir to logical coqdir\ \n -top coqdir set the toplevel name to be coqdir instead of Top\ -\n -notop set the toplevel name to be the empty logical path\ \n -exclude-dir f exclude subdirectories named f for option -R\ \n\ \n -noinit start without loading the Init library\ |