From ed18331f31fe2da5215a2548527e2b877f0b722f Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Fri, 9 Aug 2013 08:58:29 +0000
Subject: fix batch compilation of scripts containing Admitted

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16689 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/stm.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 7e8f64a019..70343c216e 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -980,7 +980,8 @@ let join_aborted_proofs () =
     if id = initial_state_id then () else
     let view = VCS.visit id in
     match view.step with
-    | `Qed ((_,VtDrop,_),eop) -> observe eop; aux view.next
+    | `Qed ((_,VtDrop,_),eop) ->
+         observe eop; Proof_global.discard_all (); aux view.next
     | `Sideff _ | `Alias _ | `Cmd _ | `Fork _ | `Qed _ -> aux view.next
   in
     aux (VCS.get_branch_pos VCS.master)
-- 
cgit v1.2.3