diff options
| author | Emilio Jesus Gallego Arias | 2020-03-26 02:26:43 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-31 05:16:22 -0400 |
| commit | b755869a7fdb34dcf7dacc9d5fd93c768d71d751 (patch) | |
| tree | 68eb026dc0f9e214afcb44739e2c617d3d5f8be6 /vernac | |
| parent | 5828dffb05022ff667f44b1ad9a89f677647e0b4 (diff) | |
[proof] Split delayed and regular proof closing functions, part II
We make the types of the delayed / non-delayed declaration path
different, as the latter is just creating futures that are forced
right away.
TTBOMK the new code should behave identically w.r.t. old one, modulo
the equation `Future.(force (from_val x)) = x`.
There are some questions as what the code is doing, but in this PR
I've opted to keep the code 100% faithful to the original one, unless
I did a mistake.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/lemmas.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacstate.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacstate.mli | 2 |
3 files changed, 4 insertions, 4 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..7c191a1f86 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -170,8 +170,8 @@ module Proof_global = struct cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~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..2c9c7ecc6f 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -74,7 +74,7 @@ module Proof_global : sig 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 |