From fbfc1b8d6e9d95fcbacd3f4ab4921d6f3b01198e Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 9 Jun 2015 13:30:35 +0200
Subject: STM: states coming from workers have no proof terminators (Close
 #4246)

Hence we reuse the ones in master.
---
 proofs/proof_global.ml  | 3 +++
 proofs/proof_global.mli | 1 +
 2 files changed, 4 insertions(+)

(limited to 'proofs')

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 50a68952eb..8677b854de 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -665,4 +665,7 @@ let freeze ~marshallable =
   | `No -> !pstates
 let unfreeze s = pstates := s; update_proof_mode ()
 let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof
+let copy_terminators ~src ~tgt =
+  assert(List.length src = List.length tgt);
+  List.map2 (fun op p -> { p with terminator = op.terminator }) src tgt
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 6a5116a9e7..88e047782c 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -197,3 +197,4 @@ type state
 val freeze : marshallable:[`Yes | `No | `Shallow] -> state
 val unfreeze : state -> unit
 val proof_of_state : state -> Proof.proof
+val copy_terminators : src:state -> tgt:state -> state
-- 
cgit v1.2.3