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 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'lib/cErrors.ml')

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"]
-- 
cgit v1.2.3