diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 20ad645ec5..1e89d6937c 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1940,7 +1940,7 @@ end = struct (* {{{ *) "goals only")) else begin let (i, ast) = r_ast in - PG_compat.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p); + PG_compat.map_proof (fun p -> Proof.focus focus_cond () i p); (* STATE SPEC: * - start : id * - return: id @@ -1996,7 +1996,7 @@ end = struct (* {{{ *) stm_fail ~st fail (fun () -> (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () -> TaskQueue.with_n_workers nworkers (fun queue -> - PG_compat.simple_with_current_proof (fun _ p -> + PG_compat.map_proof (fun p -> let Proof.{goals} = Proof.data p in let open TacTask in let res = CList.map_i (fun i g -> |