diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-07-16 17:22:54 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-07-16 17:22:54 +0200 |
| commit | 3f8aa587af3cbe33964c48a9a937e505577c4555 (patch) | |
| tree | 538f138b7251b54f1594a791bb39663ddff111e5 | |
| parent | 59e99e01a5f23f53bbfb4828e6a0639efa9235b5 (diff) | |
STM: check-vi-task fixed
| -rw-r--r-- | stm/stm.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 2895062ed..4bc7282c4 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -818,7 +818,8 @@ end = struct | Declarations.OpaqueDef lc -> let uc = Option.get (Opaqueproof.get_constraints lc) in let uc = - Future.chain ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in + Future.chain + ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in let pr = Opaqueproof.get_proof lc in let pr = Future.chain ~greedy:true ~pure:true pr discharge in let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in @@ -1573,7 +1574,8 @@ let join () = type tasks = Slaves.tasks * RemoteCounter.remote_counters_status let dump x = Slaves.dump x, RemoteCounter.backup () -let check_task name (tasks,_) i = +let check_task name (tasks,rcbackup) i = + RemoteCounter.restore rcbackup; let vcs = VCS.backup () in try let rc = Future.purify (Slaves.check_task name tasks) i in |