Merge PR #11915: [proof] Split delayed and regular proof closing functions

Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: ppedrot

10 files changed, 164 insertions, 152 deletions

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 568dfbe0f1..d38c3c869b 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -199,7 +199,7 @@ let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_
   (*    end; *)
 
   let open Proof_global in
-  let { entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in
+  let { entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false) lemma in
   match entries with
   | [entry] ->
     entry, hook
diff --git a/stm/stm.ml b/stm/stm.ml
index 62556d38ff..5b88ee3d68 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1501,7 +1501,7 @@ end = struct (* {{{ *)
       let wall_clock2 = Unix.gettimeofday () in
       Aux_file.record_in_aux_at ?loc "proof_build_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
-      let p = PG_compat.return_proof ~allow_partial:drop_pt () in
+      let p = if drop_pt then PG_compat.return_partial_proof () else PG_compat.return_proof () in
       if drop_pt then feedback ~id Complete;
       p)
 
@@ -1522,15 +1522,15 @@ end = struct (* {{{ *)
       let st = State.freeze () in
       if not drop then begin
         let checked_proof = Future.chain future_proof (fun p ->
-          let opaque = Proof_global.Opaque in
 
           (* Unfortunately close_future_proof and friends are not pure so we need
              to set the state manually here *)
           State.unfreeze st;
           let pobject, _info =
-            PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in
+            PG_compat.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in
 
           let st = Vernacstate.freeze_interp_state ~marshallable:false in
+          let opaque = Proof_global.Opaque in
           stm_qed_delay_proof ~st ~id:stop
             ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None))) in
         ignore(Future.join checked_proof);
@@ -1661,14 +1661,14 @@ end = struct (* {{{ *)
     try
       Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false stop;
       if drop then
-        let _proof = PG_compat.return_proof ~allow_partial:true () in
+        let _proof = PG_compat.return_partial_proof () in
         `OK_ADMITTED
       else begin
       let opaque = Proof_global.Opaque in
 
       (* The original terminator, a hook, has not been saved in the .vio*)
       let proof, _info =
-        PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
+        PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true in
 
       let info = Lemmas.Info.make () in
 
@@ -2479,13 +2479,13 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                           ~drop_pt exn_info block_stop, ref false
                     in
                     qed.fproof <- Some (Some fp, cancel);
-                    let opaque = match keep' with
-                      | VtKeepAxiom | VtKeepOpaque ->
-                        Proof_global.Opaque (* Admitted -> Opaque should be OK. *)
-                      | VtKeepDefined -> Proof_global.Transparent
+                    let () = match keep' with
+                      | VtKeepAxiom | VtKeepOpaque -> ()
+                      | VtKeepDefined ->
+                        CErrors.anomaly (Pp.str "Cannot delegate transparent proofs, this is a bug in the STM.")
                     in
                     let proof, info =
-                      PG_compat.close_future_proof ~opaque ~feedback_id:id fp in
+                      PG_compat.close_future_proof ~feedback_id:id fp in
                     if not delegate then ignore(Future.compute fp);
                     reach view.next;
                     let st = Vernacstate.freeze_interp_state ~marshallable:false in
@@ -2518,9 +2518,11 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                       | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent
                       | VtKeepAxiom -> assert false
                     in
-                      Some(PG_compat.close_proof ~opaque
-                                ~keep_body_ucst_separate:false
-                                (State.exn_on id ~valid:eop)) in
+                    try Some (PG_compat.close_proof ~opaque ~keep_body_ucst_separate:false)
+                    with exn ->
+                      let iexn = Exninfo.capture exn in
+                      Exninfo.iraise (State.exn_on id ~valid:eop iexn)
+                in
                 if keep <> VtKeep VtKeepAxiom then
                   reach view.next;
                 let wall_clock2 = Unix.gettimeofday () in
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 5e6f78be6f..324007930a 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -187,14 +187,14 @@ let record_aux env s_ty s_bo =
 
 let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
 
-let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
-    ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) body =
-  { proof_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
-    proof_entry_secctx = None;
+let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types
+    ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body =
+  { proof_entry_body = Future.from_val ?fix_exn ((body,univsbody), eff);
+    proof_entry_secctx = section_vars;
     proof_entry_type = types;
     proof_entry_universes = univs;
     proof_entry_opaque = opaque;
-    proof_entry_feedback = None;
+    proof_entry_feedback = feedback_id;
     proof_entry_inline_code = inline}
 
 let pure_definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 0068b9842a..615cffeae7 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -59,9 +59,14 @@ val definition_entry
   : ?fix_exn:Future.fix_exn
   -> ?opaque:bool
   -> ?inline:bool
+  -> ?feedback_id:Stateid.t
+  -> ?section_vars:Id.Set.t
   -> ?types:types
   -> ?univs:Entries.universes_entry
   -> ?eff:Evd.side_effects
+  -> ?univsbody:Univ.ContextSet.t
+  (** Universe-constraints attached to the body-only, used in
+     vio-delayed opaque constants and private poly universes *)
   -> constr
   -> Evd.side_effects proof_entry
 
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index b228a04298..22d0ce5328 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -122,7 +122,7 @@ let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ~uctx ~sig
   let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
   let pf, status = by tac pf in
   let open Proof_global in
-  let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in
+  let { entries; uctx } = close_proof ~opaque ~keep_body_ucst_separate:false pf in
   match entries with
   | [entry] ->
     entry, status, uctx
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 620afbaf23..d7dcc13e79 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -118,8 +118,7 @@ let set_used_variables ps l =
     Environ.fold_named_context aux env ~init:(ctx,ctx_set) in
   if not (Option.is_empty ps.section_vars) then
     CErrors.user_err Pp.(str "Used section variables can be declared only once");
-  (* EJGA: This is always empty thus we should modify the type *)
-  (ctx, []), { ps with section_vars = Some (Context.Named.to_vars ctx) }
+  ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) }
 
 let get_open_goals ps =
   let Proof.{ goals; stack; shelf } = Proof.data ps.proof in
@@ -141,110 +140,8 @@ let private_poly_univs =
   in
   fun () -> !b
 
-let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
-                (fpl : closed_proof_output Future.computation) ps =
-  let { section_vars; proof; udecl; initial_euctx } = ps in
-  let Proof.{ name; poly; entry } = Proof.data proof in
-  let opaque = match opaque with Opaque -> true | Transparent -> false in
-  let constrain_variables ctx =
-    UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
-  in
-  let fpl, univs = Future.split2 fpl in
-  let uctx = if poly || now then Future.force univs else initial_euctx in
-  (* Because of dependent subgoals at the beginning of proofs, we could
-     have existential variables in the initial types of goals, we need to
-     normalise them for the kernel. *)
-  let subst_evar k =
-    let { Proof.sigma } = Proof.data proof in
-    Evd.existential_opt_value0 sigma k in
-  let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar
-    (UState.subst uctx) in
-
-  let make_body =
-    if poly || now then
-      let make_body t (c, eff) =
-        let body = c in
-        let allow_deferred =
-          not poly && (keep_body_ucst_separate ||
-          not (Safe_typing.empty_private_constants = eff.Evd.seff_private))
-        in
-        let typ = if allow_deferred then t else nf t in
-        let used_univs_body = Vars.universes_of_constr body in
-        let used_univs_typ = Vars.universes_of_constr typ in
-        if allow_deferred then
-          let initunivs = UState.univ_entry ~poly initial_euctx in
-          let ctx = constrain_variables uctx in
-          (* For vi2vo compilation proofs are computed now but we need to
-             complement the univ constraints of the typ with the ones of
-             the body.  So we keep the two sets distinct. *)
-          let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let ctx_body = UState.restrict ctx used_univs in
-          let univs = UState.check_mono_univ_decl ctx_body udecl in
-          (initunivs, typ), ((body, univs), eff)
-        else if poly && opaque && private_poly_univs () then
-          let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let universes = UState.restrict uctx used_univs in
-          let typus = UState.restrict universes used_univs_typ in
-          let udecl = UState.check_univ_decl ~poly typus udecl in
-          let ubody = Univ.ContextSet.diff
-              (UState.context_set universes)
-              (UState.context_set typus)
-          in
-          (udecl, typ), ((body, ubody), eff)
-        else
-          (* Since the proof is computed now, we can simply have 1 set of
-             constraints in which we merge the ones for the body and the ones
-             for the typ. We recheck the declaration after restricting with
-             the actually used universes.
-             TODO: check if restrict is really necessary now. *)
-          let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
-          let ctx = UState.restrict uctx used_univs in
-          let univs = UState.check_univ_decl ~poly ctx udecl in
-          (univs, typ), ((body, Univ.ContextSet.empty), eff)
-      in
-       fun t p -> Future.split2 (Future.chain p (make_body t))
-    else
-      fun t p ->
-        (* Already checked the univ_decl for the type universes when starting the proof. *)
-        let univctx = UState.univ_entry ~poly:false uctx in
-        let t = nf t in
-        Future.from_val (univctx, t),
-        Future.chain p (fun (pt,eff) ->
-          (* Deferred proof, we already checked the universe declaration with
-             the initial universes, ensure that the final universes respect
-             the declaration as well. If the declaration is non-extensible,
-             this will prevent the body from adding universes and constraints. *)
-          let univs = Future.force univs in
-          let univs = constrain_variables univs in
-          let used_univs = Univ.LSet.union
-              (Vars.universes_of_constr t)
-              (Vars.universes_of_constr pt)
-          in
-          let univs = UState.restrict univs used_univs in
-          let univs = UState.check_mono_univ_decl univs udecl in
-          (pt,univs),eff)
-  in
-  let entry_fn p (_, t) =
-    let t = EConstr.Unsafe.to_constr t in
-    let univstyp, body = make_body t p in
-    let univs, typ = Future.force univstyp in
-    Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types:typ body
-  in
-  let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in
-  { name; entries; uctx }
-
-let return_proof ?(allow_partial=false) ps =
- let { proof } = ps in
- if allow_partial then begin
-  let proofs = Proof.partial_proof proof in
-  let Proof.{sigma=evd} = Proof.data proof in
-  let eff = Evd.eval_side_effects evd in
-  (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
-     side-effects... This may explain why one need to uniquize side-effects
-     thereafter... *)
-  let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
-    proofs, Evd.evar_universe_context evd
- end else
+(* XXX: This is still separate from close_proof below due to drop_pt in the STM *)
+let return_proof { proof } =
   let Proof.{name=pid;entry} = Proof.data proof in
   let initial_goals = Proofview.initial_goals entry in
   let evd = Proof.return ~pid proof in
@@ -266,16 +163,122 @@ let return_proof ?(allow_partial=false) ps =
      code-paths that generate several proof entries are derive and
      equations and so far there is no code in the CI that will
      actually call those and do a side-effect, TTBOMK *)
-  let proofs =
-    List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in
-    proofs, Evd.evar_universe_context evd
+  (* EJGA: likely the right solution is to attach side effects to the first constant only? *)
+  let proofs = List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in
+  proofs, Evd.evar_universe_context evd
+
+let close_proof ~opaque ~keep_body_ucst_separate ps =
+  let elist, uctx = return_proof ps in
+  let { section_vars; proof; udecl; initial_euctx } = ps in
+  let { Proof.name; poly; entry; sigma } = Proof.data proof in
+  let opaque = match opaque with Opaque -> true | Transparent -> false in
+
+  (* Because of dependent subgoals at the beginning of proofs, we could
+     have existential variables in the initial types of goals, we need to
+     normalise them for the kernel. *)
+  let subst_evar k = Evd.existential_opt_value0 sigma k in
+  let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst uctx) in
+
+  let make_entry (body, eff) (_, typ) =
+    let allow_deferred =
+      not poly && (keep_body_ucst_separate ||
+                   not (Safe_typing.empty_private_constants = eff.Evd.seff_private))
+    in
+    (* EJGA: Why are we doing things this way? *)
+    let typ = EConstr.Unsafe.to_constr typ in
+    let typ = if allow_deferred then typ else nf typ in
+    (* EJGA: End "Why are we doing things this way?" *)
+
+    let used_univs_body = Vars.universes_of_constr body in
+    let used_univs_typ = Vars.universes_of_constr typ in
+    let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+    let utyp, ubody =
+      if allow_deferred then
+        let utyp = UState.univ_entry ~poly initial_euctx in
+        let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
+        (* For vi2vo compilation proofs are computed now but we need to
+           complement the univ constraints of the typ with the ones of
+           the body.  So we keep the two sets distinct. *)
+        let uctx_body = UState.restrict uctx used_univs in
+        let ubody = UState.check_mono_univ_decl uctx_body udecl in
+        utyp, ubody
+      else if poly && opaque && private_poly_univs () then
+        let universes = UState.restrict uctx used_univs in
+        let typus = UState.restrict universes used_univs_typ in
+        let utyp = UState.check_univ_decl ~poly typus udecl in
+        let ubody = Univ.ContextSet.diff
+            (UState.context_set universes)
+            (UState.context_set typus)
+        in
+        utyp, ubody
+      else
+        (* Since the proof is computed now, we can simply have 1 set of
+           constraints in which we merge the ones for the body and the ones
+           for the typ. We recheck the declaration after restricting with
+           the actually used universes.
+           TODO: check if restrict is really necessary now. *)
+        let ctx = UState.restrict uctx used_univs in
+        let utyp = UState.check_univ_decl ~poly ctx udecl in
+        utyp, Univ.ContextSet.empty
+    in
+    Declare.definition_entry ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
+  in
+  let entries = CList.map2 make_entry elist (Proofview.initial_goals entry) in
+  { name; entries; uctx }
+
+let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) =
+  let { section_vars; proof; udecl; initial_euctx } = ps in
+  let { Proof.name; poly; entry; sigma } = Proof.data proof in
 
-let close_future_proof ~opaque ~feedback_id ps proof =
-  close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof ps
+  (* We don't allow poly = true in this path *)
+  if poly then
+    CErrors.anomaly (Pp.str "Cannot delay universe-polymorphic constants.");
 
-let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps =
-  close_proof ~opaque ~keep_body_ucst_separate ~now:true
-    (Future.from_val ~fix_exn (return_proof ps)) ps
+  let fpl, uctx = Future.split2 fpl in
+  (* Because of dependent subgoals at the beginning of proofs, we could
+     have existential variables in the initial types of goals, we need to
+     normalise them for the kernel. *)
+  let subst_evar k = Evd.existential_opt_value0 sigma k in
+  let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst initial_euctx) in
+
+  (* We only support opaque proofs, this will be enforced by using
+     different entries soon *)
+  let opaque = true in
+  let make_entry p (_, types) =
+    (* Already checked the univ_decl for the type universes when starting the proof. *)
+    let univs = UState.univ_entry ~poly:false initial_euctx in
+    let types = nf (EConstr.Unsafe.to_constr types) in
+
+    Future.chain p (fun (pt,eff) ->
+        (* Deferred proof, we already checked the universe declaration with
+             the initial universes, ensure that the final universes respect
+             the declaration as well. If the declaration is non-extensible,
+             this will prevent the body from adding universes and constraints. *)
+        let uctx = Future.force uctx in
+        let uctx = UState.constrain_variables (fst (UState.context_set initial_euctx)) uctx in
+        let used_univs = Univ.LSet.union
+            (Vars.universes_of_constr types)
+            (Vars.universes_of_constr pt)
+        in
+        let univs = UState.restrict uctx used_univs in
+        let univs = UState.check_mono_univ_decl univs udecl in
+        (pt,univs),eff)
+    |> Declare.delayed_definition_entry ~opaque ~feedback_id ?section_vars ~univs ~types
+  in
+  let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in
+  { name; entries; uctx = initial_euctx }
+
+let close_future_proof = close_proof_delayed
+
+let return_partial_proof { proof } =
+ let proofs = Proof.partial_proof proof in
+ let Proof.{sigma=evd} = Proof.data proof in
+ let eff = Evd.eval_side_effects evd in
+ (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+     side-effects... This may explain why one need to uniquize side-effects
+     thereafter... *)
+ let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
+ proofs, Evd.evar_universe_context evd
 
 let update_global_env =
   map_proof (fun p ->
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index d820fc8b40..874708ded8 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -67,7 +67,7 @@ val update_global_env : t -> t
 
 (* Takes a function to add to the exceptions data relative to the
    state in which the proof was built *)
-val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> proof_object
+val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> t -> proof_object
 
 (* Intermediate step necessary to delegate the future.
  * Both access the current proof state. The former is supposed to be
@@ -75,11 +75,13 @@ val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.
 
 type closed_proof_output
 
-(* If allow_partial is set (default no) then an incomplete proof
- * is allowed (no error), and a warn is given if the proof is complete. *)
-val return_proof : ?allow_partial:bool -> t -> closed_proof_output
-val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t ->
-  closed_proof_output Future.computation -> proof_object
+(** Requires a complete proof. *)
+val return_proof : t -> closed_proof_output
+
+(** An incomplete proof is allowed (no error), and a warn is given if
+   the proof is complete. *)
+val return_partial_proof : t -> closed_proof_output
+val close_future_proof : feedback_id:Stateid.t -> t -> closed_proof_output Future.computation -> proof_object
 
 val get_open_goals : t -> int
 
@@ -91,7 +93,6 @@ val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a)
 val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
 
 (** Sets the section variables assumed by the proof, returns its closure
- * (w.r.t. type dependencies and let-ins covered by it) + a list of
- * ids to be cleared *)
+ * (w.r.t. type dependencies and let-ins covered by it) *)
 val set_used_variables : t ->
-  Names.Id.t list -> (Constr.named_context * Names.lident list) * t
+  Names.Id.t list -> Constr.named_context * t
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