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 /vernac/vernacstate.ml | |
| 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 'vernac/vernacstate.ml')
| -rw-r--r-- | vernac/vernacstate.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index af68ef88cf..c51d3c30f4 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -121,12 +121,12 @@ module Proof_global = struct let give_me_the_proof () = cc get_proof let get_current_proof_name () = cc get_proof_name - let simple_with_current_proof f = dd (Proof_global.simple_with_proof f) + let map_proof f = dd (map_proof f) let with_current_proof f = match !s_lemmas with | None -> raise NoCurrentProof | Some stack -> - let pf, res = Stack.with_top_pstate stack ~f:(with_proof f) in + let pf, res = Stack.with_top_pstate stack ~f:(map_fold_proof_endline f) in let stack = Stack.map_top_pstate stack ~f:(fun _ -> pf) in s_lemmas := Some stack; res |