diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-03-26 14:01:52 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-03-26 14:01:52 +0200 |
| commit | c1dcb97cf95c10d19f67689108da8726232da4fb (patch) | |
| tree | 54b60698a12d133cccd822f323cec582ac0e9e6a /stm | |
| parent | e128900aee63c972d7977fd47e3fd21649b63409 (diff) | |
| parent | 75f569f35fbbbbab5a4629eaf3385335a3024e0b (diff) | |
Merge PR #6970: [vernac] Move `Quit` and `Drop` to the toplevel layer.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 6 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 1 |
2 files changed, 0 insertions, 7 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index dbecbdae5..4b49d1998 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; @@ -2886,11 +2885,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 diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f68c8b326..9a8af3a58 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -185,7 +185,6 @@ let classify_vernac e = | VernacResetName _ | VernacResetInitial | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow (* What are these? *) - | VernacToplevelControl _ | VernacRestoreState _ | VernacWriteState _ -> VtSideff [], VtNow (* Plugins should classify their commands *) |