diff options
Diffstat (limited to 'vernac/vernacstate.ml')
| -rw-r--r-- | vernac/vernacstate.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 6846826bfa..a4e9c8e1ab 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -164,14 +164,15 @@ 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, + let close_future_proof ~feedback_id pf = + cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~feedback_id st pf) pt, Internal.get_info 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, + let close_proof ~opaque ~keep_body_ucst_separate = + cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate)) pt, Internal.get_info pt) let discard_all () = s_lemmas := None |