From 7135ab891d130dcce9e1d52fc2687bc569397e2b Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Tue, 1 Oct 2013 15:35:31 +0000
Subject: STM: fully force a proof ourput before sending it back to the master

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

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index a15b31da47..bc16077b93 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -717,7 +717,16 @@ end = struct (* {{{ *)
     | ReqBuildProof(exn_info,eop, vcs) ->
         VCS.restore vcs;
         VCS.print ();
-        let r = RespBuiltProof (Future.force (build_proof_here exn_info eop)) in
+        let r = RespBuiltProof (
+          let l = Future.force (build_proof_here exn_info eop) in
+          List.iter (fun (_,se) -> Declareops.iter_side_effects (function
+            | Declarations.SEsubproof(_,
+               { Declarations.const_body = Declarations.OpaqueDef f;
+                 const_constraints = cst} ) -> 
+                  ignore(Future.force f); ignore(Future.force cst)
+            | _ -> ())
+          se) l;
+          l) in
         VCS.print ();
         r
 
-- 
cgit v1.2.3