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

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 .
---
 toplevel/coqtop.ml | 8 +++-----
 toplevel/usage.ml  | 1 -
 2 files changed, 3 insertions(+), 6 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index cc1c44fe31..c9a1f0def5 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 38ceacf5ec..66f782ffbe 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\
-- 
cgit v1.2.3