diff options
| author | Emilio Jesus Gallego Arias | 2019-02-14 12:45:49 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-09 14:26:58 +0200 |
| commit | cb84805a1758ab52506f74207dacd80a8f07224e (patch) | |
| tree | 40b735ebbf6bde70df2ab8636a073b82262a4db2 /vernac/vernacstate.ml | |
| parent | a8b3c907cb2d6da16bdeea10b943552dc9efc0ed (diff) | |
[save_proof] Make terminator API internal.
We refactor the terminator API to make it more internal. Indeed we
remove `set_terminator` and `get_terminator` is only there due to
access to internals in the STM `save_proof` path by the infamous
`?proof` parameter.
After this only 2 non-standard terminators remain: obligations and
derive. We will refactor those in next PRs.
Diffstat (limited to 'vernac/vernacstate.ml')
| -rw-r--r-- | vernac/vernacstate.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 90075cbb70..af68ef88cf 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -114,14 +114,9 @@ module Proof_global = struct | None -> raise NoCurrentProof | Some x -> s_lemmas := Some (Stack.map_top_pstate ~f x) - let dd_lemma f = match !s_lemmas with - | None -> raise NoCurrentProof - | Some x -> s_lemmas := Some (Stack.map_top ~f x) - let there_are_pending_proofs () = !s_lemmas <> None let get_open_goals () = cc get_open_goals - let set_terminator x = dd_lemma (set_terminator x) let give_me_the_proof_opt () = Option.map (Stack.with_top_pstate ~f:get_proof) !s_lemmas let give_me_the_proof () = cc get_proof let get_current_proof_name () = cc get_proof_name @@ -143,11 +138,11 @@ module Proof_global = struct let close_future_proof ~opaque ~feedback_id pf = cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt, - get_terminator pt) + Internal.get_terminator pt) let close_proof ~opaque ~keep_body_ucst_separate f = cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate f)) pt, - get_terminator pt) + Internal.get_terminator pt) let discard_all () = s_lemmas := None let update_global_env () = dd (update_global_env) |