STM: if a-p-always-delegate fetch states from parked worker on edit-at

If the async-proofs-always-delegate is passed, workers are killed
only when the proof they computed is obsolete.  If one jumps back
to a state that was computed by the worker (and not the master) instead
of (re)computing such state in the master ask the worker to send it
back.

1 files changed, 5 insertions, 5 deletions

diff --git a/stm/vcs.ml b/stm/vcs.ml
index e2513b1c1..3efe89358 100644
--- a/stm/vcs.ml
+++ b/stm/vcs.ml
@@ -62,11 +62,11 @@ module type S = sig
   val reachable : ('k,'e,'info) t -> id -> NodeSet.t
 
   module Dag : Dag.S with type node = id
-  val dag : ('kind,'diff,'info) t -> ('diff,'info,id) Dag.t
+  val dag : ('kind,'diff,'info) t -> ('diff,'info,id*id) Dag.t
 
-  val create_cluster : ('k,'e,'i) t -> id list -> id -> ('k,'e,'i) t
-  val cluster_of : ('k,'e,'i) t -> id -> id Dag.Cluster.t option
-  val delete_cluster : ('k,'e,'i) t -> id Dag.Cluster.t -> ('k,'e,'i) t 
+  val create_cluster : ('k,'e,'i) t -> id list -> (id * id) -> ('k,'e,'i) t
+  val cluster_of : ('k,'e,'i) t -> id -> (id * id) Dag.Cluster.t option
+  val delete_cluster : ('k,'e,'i) t -> (id * id) Dag.Cluster.t -> ('k,'e,'i) t 
 
 end
 
@@ -102,7 +102,7 @@ type 'kind branch_info = {
 type ('kind,'edge,'info) t = {
   cur_branch   : Branch.t;
   heads        : 'kind branch_info BranchMap.t;
-  dag          : ('edge,'info,id) Dag.t;
+  dag          : ('edge,'info,id*id) Dag.t;
 }
 
 let empty root = {