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.ml  | 4 +---
 lib/cErrors.mli | 2 --
 2 files changed, 1 insertion(+), 5 deletions(-)

(limited to 'lib')

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 9750221143..811fcf4063 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -47,8 +47,6 @@ exception AlreadyDeclared of Pp.t (* for already declared Schemes *)
 let alreadydeclared pps = raise (AlreadyDeclared(pps))
 
 exception Timeout
-exception Drop
-exception Quit
 
 let handle_stack = ref []
 
@@ -126,7 +124,7 @@ end
 let noncritical = function
   | Sys.Break | Out_of_memory | Stack_overflow
   | Assert_failure _ | Match_failure _ | Anomaly _
-  | Timeout | Drop | Quit -> false
+  | Timeout -> false
   | Invalid_argument "equal: functional value" -> false
   | _ -> true
 [@@@ocaml.warning "+52"]
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