diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-14 21:24:53 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-14 21:24:53 +0100 |
| commit | b087d133f7d6d091cce72190c05a9a09d5b37791 (patch) | |
| tree | c9cd3ce85a71aba2b48d34aca58bf5ac573c8471 /toplevel/usage.ml | |
| parent | 93a75d635ac3fb52eed7b39c3c7a8e656f0a81b7 (diff) | |
[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 .
Diffstat (limited to 'toplevel/usage.ml')
| -rw-r--r-- | toplevel/usage.ml | 1 |
1 files changed, 0 insertions, 1 deletions
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\ |