diff options
| author | Enrico Tassi | 2015-02-20 16:01:12 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-02-21 19:25:24 +0100 |
| commit | 7fc3adcf583cea7db6a224d9a58554b19d41cd4c (patch) | |
| tree | 7ffc7fd9192d4e4ab8f469b1c66a6aaa4e7f73a8 /stm | |
| parent | cab07133acbce19e865b8302fef24dd4ea190d90 (diff) | |
Future: human readable name for delegated (Close #4065)
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 43db6f3f6c..a4db934b25 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1270,7 +1270,7 @@ end = struct (* {{{ *) if TaskQueue.n_workers (Option.get !queue) = 0 then if !Flags.compilation_mode = Flags.BuildVio then begin let f,assign = - Future.create_delegate ~blocking:true (State.exn_on id ~valid) in + Future.create_delegate ~blocking:true ~name:pname (State.exn_on id ~valid) in let t_uuid = Future.uuid f in let task = ProofTask.(BuildProof { t_exn_info; t_start = start; t_stop = stop; @@ -1281,7 +1281,7 @@ end = struct (* {{{ *) end else ProofTask.build_proof_here t_exn_info loc stop, cancel_switch else - let f, t_assign = Future.create_delegate (State.exn_on id ~valid) in + let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in let t_uuid = Future.uuid f in feedback (Feedback.InProgress 1); let task = ProofTask.(BuildProof { @@ -1436,7 +1436,10 @@ end = struct (* {{{ *) let goals, _, _, _, _ = Proof.proof p in let open TacTask in let res = CList.map_i (fun i g -> - let f,assign= Future.create_delegate (State.exn_on id ~valid:safe_id) in + let f, assign = + Future.create_delegate + ~name:(Printf.sprintf "subgoal %d" i) + (State.exn_on id ~valid:safe_id) in let t_ast = { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } in let t_name = Goal.uid g in |