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/vernacstate.ml | |
| 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/vernacstate.ml')
| -rw-r--r-- | vernac/vernacstate.ml | 3 |
1 files changed, 2 insertions, 1 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, |