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. --- stm/stm.ml | 6 ------ 1 file changed, 6 deletions(-) (limited to 'stm/stm.ml') diff --git a/stm/stm.ml b/stm/stm.ml index ad94b6807..756b93c61 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2734,7 +2734,6 @@ let merge_proof_branch ~valid ?id qast keep brname = (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) let handle_failure (e, info) vcs = - if e = CErrors.Drop then Exninfo.iraise (e, info) else match Stateid.get info with | None -> VCS.restore vcs; @@ -2881,11 +2880,6 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) rc (* Side effect on all branches *) - | VtUnknown, _ when Vernacprop.under_control expr = VernacToplevelControl Drop -> - let st = Vernacstate.freeze_interp_state `No in - ignore(stm_vernac_interp (VCS.get_branch_pos head) st x); - `Ok - | VtSideff l, w -> let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in let id = VCS.new_node ~id:newtip () in -- cgit v1.2.3