diff options
| author | Emilio Jesus Gallego Arias | 2020-03-26 02:45:47 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-31 05:16:22 -0400 |
| commit | e9c05828bba7ceb696a5c17457b8e0826bbd94f1 (patch) | |
| tree | fa9f93732095d304aff28239b7293ae6c1bbb075 /vernac | |
| parent | b755869a7fdb34dcf7dacc9d5fd93c768d71d751 (diff) | |
[proof] Split return_proof in partial and regular versions.
This is a small refactoring as these two functions behave very
differently and the invariants are quite different, in fact regular
`return_proof` should not be exported but be part of close proof, but
there is small use in the STM still.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacstate.ml | 3 | ||||
| -rw-r--r-- | vernac/vernacstate.mli | 3 |
2 files changed, 4 insertions, 2 deletions
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 7c191a1f86..b722acd1ad 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -164,7 +164,8 @@ module Proof_global = struct type closed_proof = Proof_global.proof_object * Lemmas.Info.t - let return_proof ?allow_partial () = cc (return_proof ?allow_partial) + let return_proof () = cc return_proof + let return_partial_proof () = cc return_partial_proof 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, diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index 2c9c7ecc6f..b6b24c9275 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -65,7 +65,8 @@ module Proof_global : sig 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 + val return_proof : unit -> Proof_global.closed_proof_output + val return_partial_proof : unit -> Proof_global.closed_proof_output type closed_proof = Proof_global.proof_object * Lemmas.Info.t |