From fe727711d9d48b97505179c611d45cbbec6545ab Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Fri, 9 Aug 2013 12:41:22 +0000
Subject: Fix batch compilation of scripts with Admitted proofs (in a section)

This time all collateral effects of forcing the execution
of dropped proofs should be handled correctly

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

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