diff options
| author | Enrico Tassi | 2014-07-16 15:02:48 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-07-16 15:02:55 +0200 |
| commit | 59e99e01a5f23f53bbfb4828e6a0639efa9235b5 (patch) | |
| tree | 663f0e1171a4f62dc22aa4f58f1170d3b1a1c02a | |
| parent | 1ca444867477e471f2fd04c1abd610d3fceb96d9 (diff) | |
STM: Goal printing got wrong in a merge, fixed
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 4d29bbb38e..2895062edf 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -733,6 +733,7 @@ end = struct let slave_print_all_goals id = let rec aux id = + print_goals_of_state id; try aux (VCS.visit id).next with | VCS.Expired -> () @@ -1368,7 +1369,8 @@ let known_state ?(redefine_qed=false) ~cache id = if !Flags.async_proofs_mode = Flags.APonParallel 0 then Pp.feedback ~state_id:id Feedback.ProcessingInMaster; State.define ~cache:cache_step ~redefine:redefine_qed step id; - if !Flags.feedback_goals then print_goals_of_state id; + if !Flags.feedback_goals && not (Flags.async_proofs_is_worker ()) then + print_goals_of_state id; prerr_endline ("reached: "^ Stateid.to_string id) in reach ~redefine_qed id |