From 75f569f35fbbbbab5a4629eaf3385335a3024e0b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 11 Mar 2018 03:16:09 +0100
Subject: [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.
---
 intf/vernacexpr.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index df061bfb72..dc1110ad86 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
-- 
cgit v1.2.3