diff options
| author | Pierre-Marie Pédrot | 2020-03-31 21:53:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-31 21:53:51 +0200 |
| commit | e98e8a03cae984a10fddc8acbe8fd781d4608b24 (patch) | |
| tree | 69e9890126ce32c0c856a35661365b88d5a9d1ae /vernac | |
| parent | ee82486472f39cbe4760a3e586d9efb152e85c24 (diff) | |
| parent | 7afd5e9fb7ba9e5fc41e41fd54eb90ee8cb13993 (diff) | |
Merge PR #11915: [proof] Split delayed and regular proof closing functions
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/lemmas.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacstate.ml | 11 | ||||
| -rw-r--r-- | vernac/vernacstate.mli | 6 |
3 files changed, 10 insertions, 9 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index feedf4d71d..7f7340bb34 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -403,7 +403,7 @@ let process_idopt_for_save ~idopt info = let save_lemma_proved ~lemma ~opaque ~idopt = (* Env and sigma are just used for error printing in save_remaining_recthms *) - let proof_obj = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) lemma.proof in + let proof_obj = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false lemma.proof in let proof_info = process_idopt_for_save ~idopt lemma.info in finalize_proof proof_obj proof_info 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 diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index 7607f8373a..9c4de7720c 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -65,16 +65,16 @@ 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 val close_future_proof : - opaque:Proof_global.opacity_flag -> feedback_id:Stateid.t -> Proof_global.closed_proof_output Future.computation -> closed_proof - val close_proof : opaque:Proof_global.opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof + val close_proof : opaque:Proof_global.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof val discard_all : unit -> unit val update_global_env : unit -> unit |