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.mli | |
| 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.mli')
| -rw-r--r-- | vernac/vernacstate.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index bfa85e022c..9f4e366e1c 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -45,13 +45,10 @@ module Proof_global : sig val give_me_the_proof_opt : unit -> Proof.t option val get_current_proof_name : unit -> Names.Id.t - val simple_with_current_proof : - (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit - + val map_proof : (Proof.t -> Proof.t) -> unit val with_current_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a - val return_proof : ?allow_partial:bool -> unit -> Proof_global.closed_proof_output type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator |