aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-03-14 21:24:53 +0100
committerEmilio Jesus Gallego Arias2017-03-14 21:24:53 +0100
commitb087d133f7d6d091cce72190c05a9a09d5b37791 (patch)
treec9cd3ce85a71aba2b48d34aca58bf5ac573c8471 /kernel/nativelambda.ml
parent93a75d635ac3fb52eed7b39c3c7a8e656f0a81b7 (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 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions