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 .
---
 doc/refman/RefMan-ext.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/refman/RefMan-ext.tex')

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index b475a5233c..1d423f8b16 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