diff options
| author | Emilio Jesus Gallego Arias | 2019-05-22 17:29:22 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-09 14:26:58 +0200 |
| commit | 879475156ccbfb14687ed9a02b04f8cf2422d698 (patch) | |
| tree | f582f419374c6d249b64e77ba7fd81123fea2c76 /stm | |
| parent | cb84805a1758ab52506f74207dacd80a8f07224e (diff) | |
[proof] Uniformize Proof_global API
We rename modify to map [more in line with the rest of the system] and
make the endline function specific, as it is only used in one case.
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 -> |