diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-06-09 13:30:35 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-06-09 13:30:35 +0200 |
| commit | fbfc1b8d6e9d95fcbacd3f4ab4921d6f3b01198e (patch) | |
| tree | 75417b1dfa1720e28c265105a06e3fb23dc85847 /proofs/proof_global.ml | |
| parent | a7a1ec22bc2aa06cc419f7012863656c3aec5871 (diff) | |
STM: states coming from workers have no proof terminators (Close #4246)
Hence we reuse the ones in master.
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 50a68952e..8677b854d 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 |