[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.

10 files changed, 73 insertions, 77 deletions

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 45c46c56f4..0ed04d262a 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..ba8eba0eed 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1668,7 +1668,7 @@ end = struct (* {{{ *)
 
       (* 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
 
@@ -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..a149850a64 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) ?(univc=Univ.ContextSet.empty) body =
+  { proof_entry_body = Future.from_val ?fix_exn ((body,univc), 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..6ea08d5b0e 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
+  -> ?univc:Univ.ContextSet.t
+  (** Universe-constraints attached to the body-only, used in vio /
+     vio-delayed opaque constants *)
   -> 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 b97acdafa6..8d62d1635d 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -142,78 +142,73 @@ let private_poly_univs =
   fun () -> !b
 
 let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id
-                (fpl : closed_proof_output Future.computation) ps =
+                ((elist, uctx) : closed_proof_output) ps =
   let { section_vars; proof; udecl; initial_euctx } = ps in
-  let Proof.{ name; poly; entry } = Proof.data proof in
+  let Proof.{ name; poly; entry; sigma } = 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 = Future.force univs 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 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_body t (c, eff) =
+  let make_body typ (c, eff) :
+    Constr.types Entries.in_universes_entry * Evd.side_effects Entries.proof_output =
     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 typ = if allow_deferred then typ else nf typ 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)
+    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 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 ctx_body = UState.restrict ctx used_univs in
+        let univs = UState.check_mono_univ_decl ctx_body udecl in
+        utyp, univs
+      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
+    (typ, utyp), ((body, ubody), eff)
   in
-  let make_body t p = Future.split2 (Future.chain p (make_body t)) 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
+    let (typ, univs), ((body,univc),eff) = make_body t p in
+    Declare.definition_entry ~opaque ?feedback_id ?section_vars ~univs ~univc ~types:typ ~eff body
   in
-  let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in
-  { name; entries; uctx; udecl }
+  let entries = CList.map2 entry_fn elist (Proofview.initial_goals entry) in
+  { name; entries; uctx }
 
 let close_proof_delayed ~opaque ~keep_body_ucst_separate ?feedback_id
                 (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 Proof.{ name; poly; entry; sigma } = Proof.data proof in
 
   (* We don't allow poly = true in this path *)
   if poly then
@@ -228,18 +223,14 @@ let close_proof_delayed ~opaque ~keep_body_ucst_separate ?feedback_id
   (* 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 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_body 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),
+    (t, univctx),
     Future.chain p (fun (pt,eff) ->
         (* Deferred proof, we already checked the universe declaration with
            the initial universes, ensure that the final universes respect
@@ -257,9 +248,8 @@ let close_proof_delayed ~opaque ~keep_body_ucst_separate ?feedback_id
   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
+    let (typ, utyp), body = make_body t p in
+    Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs:utyp ~types:typ body
   in
   let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in
   { name; entries; uctx }
@@ -304,9 +294,8 @@ let return_proof ?(allow_partial=false) ps =
 let close_future_proof ~opaque ~feedback_id ps proof =
   close_proof_delayed ~opaque ~keep_body_ucst_separate:true ~feedback_id proof ps
 
-let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps =
-  close_proof ~opaque ~keep_body_ucst_separate
-    (Future.from_val ~fix_exn (return_proof ps)) ps
+let close_proof ~opaque ~keep_body_ucst_separate ps =
+  close_proof ~opaque ~keep_body_ucst_separate (return_proof ps) ps
 
 let update_global_env =
   map_proof (fun p ->
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index d820fc8b40..44b78ee911 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
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