diff options
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 |