From 3d2582eeb492fb21b7136016bf4c1a0463dc15c2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 1 Jul 2014 14:34:17 +0200
Subject: Patch from Enrico Tassi to get Drop compatible with stm.

---
 stm/stm.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/stm/stm.ml b/stm/stm.ml
index 4a409c0852..f62bae4b12 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1602,6 +1602,7 @@ let merge_proof_branch 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 vcs tty =
+  if e = Errors.Drop then raise e else
   match Stateid.get e with
   | None ->
       VCS.restore vcs;
@@ -1740,6 +1741,9 @@ let process_transaction ~tty verbose c (loc, expr) =
           rc
           
       (* Side effect on all branches *)
+      | VtUnknown, _ when expr = VernacToplevelControl Drop ->
+          vernac_interp (VCS.get_branch_pos head) x; `Ok
+
       | VtSideff l, w ->
           let id = VCS.new_node () in
           VCS.checkout VCS.Branch.master;
-- 
cgit v1.2.3