[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 .

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