diff options
| author | Enrico Tassi | 2015-06-09 13:30:35 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-06-09 13:30:35 +0200 |
| commit | fbfc1b8d6e9d95fcbacd3f4ab4921d6f3b01198e (patch) | |
| tree | 75417b1dfa1720e28c265105a06e3fb23dc85847 /stm | |
| parent | a7a1ec22bc2aa06cc419f7012863656c3aec5871 (diff) | |
STM: states coming from workers have no proof terminators (Close #4246)
Hence we reuse the ones in master.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index a6b21bcd9e..373fd0ba39 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -671,11 +671,22 @@ end = struct (* {{{ *) let assign id what = if VCS.get_state id <> None then () else try match what with - | `Full s -> VCS.set_state id s + | `Full s -> + let s = + try + let prev = (VCS.visit id).next in + if is_cached prev + then { s with proof = + Proof_global.copy_terminators + ~src:(get_cached prev).proof ~tgt:s.proof } + else s + with VCS.Expired -> s in + VCS.set_state id s | `Proof(ontop,(pstate,counters)) -> if is_cached ontop then let s = get_cached ontop in - let s = { s with proof = pstate } in + let s = { s with proof = + Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in let s = { s with system = States.replace_summary s.system (Summary.surgery_summary @@ -1119,7 +1130,7 @@ end = struct (* {{{ *) when is_tac expr && State.same_env o n -> (* A pure tactic *) Some (id, `Proof (prev, State.proof_part_of_frozen n)) | Some _, Some s -> - msg_warning (str "Sending back a fat state"); + msg_warning (str "STM: sending back a fat state"); Some (id, `Full s) | _, Some s -> Some (id, `Full s) in let rec aux seen = function |