diff options
| author | Pierre-Marie Pédrot | 2015-02-23 11:08:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-23 11:08:27 +0100 |
| commit | 95d1ba0636d95e213f327fc9dba9002b29e95da6 (patch) | |
| tree | fa70e88054365c1bd97976ee64199ef36021f441 /stm | |
| parent | f1389e10e6bf15e0fe3fd120f4aa8e59579a16b4 (diff) | |
| parent | f7dfa9d5e1195b8db3711126f953c1605e8cfcf2 (diff) | |
Merge branch 'v8.5'
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 |