diff options
| author | gareuselesinge | 2013-10-01 15:35:31 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-10-01 15:35:31 +0000 |
| commit | 7135ab891d130dcce9e1d52fc2687bc569397e2b (patch) | |
| tree | 33b223a1e98f47ed79767030a4363c4297b49e78 | |
| parent | 22180c5e0894bca2a2a337cea0fb494dc8609200 (diff) | |
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
| -rw-r--r-- | toplevel/stm.ml | 11 |
1 files changed, 10 insertions, 1 deletions
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 |