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.
---
 lib/cErrors.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'lib/cErrors.mli')

diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index ec34dd62c5..4e2fe7621d 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -53,8 +53,6 @@ val invalid_arg : ?loc:Loc.t -> string -> 'a
 val todo : string -> unit
 
 exception Timeout
-exception Drop
-exception Quit
 
 (** [register_handler h] registers [h] as a handler.
     When an expression is printed with [print e], it
-- 
cgit v1.2.3