From b755869a7fdb34dcf7dacc9d5fd93c768d71d751 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 26 Mar 2020 02:26:43 -0400
Subject: [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.
---
 vernac/lemmas.ml       | 2 +-
 vernac/vernacstate.ml  | 4 ++--
 vernac/vernacstate.mli | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'vernac')

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
-- 
cgit v1.2.3