diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/stm.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 67e855327b..9310591416 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -631,7 +631,9 @@ end = struct (* {{{ *) let build_proof_here (id,valid) eop = Future.create (fun () -> !reach_known_state ~cache:false eop; - Proof_global.return_proof ~fix_exn:(State.exn_on id ~valid)) + let p = Proof_global.return_proof ~fix_exn:(State.exn_on id ~valid) in + Pp.feedback (Interface.InProgress ~-1); + p) let slave_respond msg = match msg with @@ -680,6 +682,7 @@ end = struct (* {{{ *) build_proof_here exn_info stop else let f, assign = Future.create_delegate () in + Pp.feedback (Interface.InProgress 1); TQueue.push queue (TaskBuildProof(exn_info,start,stop,assign)); f |