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. --- vernac/vernacentries.ml | 3 --- 1 file changed, 3 deletions(-) (limited to 'vernac/vernacentries.ml') diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3dbe8b0c0..9ff4e3302 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2010,9 +2010,6 @@ let interp ?proof ~atts ~st c = | VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command") | VernacBacktrack _ -> CErrors.user_err (str "Backtrack cannot be used through the Load command") - (* Toplevel control *) - | VernacToplevelControl e -> raise e - (* Resetting *) | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.") -- cgit v1.2.3