aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-11 03:16:09 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-11 08:59:58 +0100
commit75f569f35fbbbbab5a4629eaf3385335a3024e0b (patch)
tree3faa24d7bec202affef352dff09cbbffbd31b26f /intf
parent33c5d8d00cb017c61141ee0d6b7cb8f672a3e691 (diff)
[vernac] Move `Quit` and `Drop` to the toplevel layer.
This is a first step towards moving REPL-specific commands out of the core layers. In particular, we remove `Quit` and `Drop` from the core vernacular to specific toplevel-level parsing rules.
Diffstat (limited to 'intf')
-rw-r--r--intf/vernacexpr.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index df061bfb7..dc1110ad8 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -457,8 +457,6 @@ type nonrec vernac_expr =
| VernacCheckGuard
| VernacProof of Genarg.raw_generic_argument option * section_subset_expr option
| VernacProofMode of string
- (* Toplevel control *)
- | VernacToplevelControl of exn
(* For extension *)
| VernacExtend of extend_name * Genarg.raw_generic_argument list