From 5828dffb05022ff667f44b1ad9a89f677647e0b4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 26 Mar 2020 01:59:05 -0400
Subject: [proof] Split delayed and regular proof closing functions, part I

We split the `close_proof` into two variants, one for delayed proof,
and one for the regular proof closing path, _à la_ interactive.

This makes sense as the typing in both cases is different, even if we
still haven't changed it.

We strongly enforce the invariant (for now) that universe polymorphic
proofs cannot be delayed using this API, as the STM expects.

It introduces some minimal, non-interesting code duplication, which
will go away in the next commits.
---
 tactics/proof_global.ml | 161 +++++++++++++++++++++++++++++-------------------
 1 file changed, 96 insertions(+), 65 deletions(-)

diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 620afbaf23..b97acdafa6 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -141,7 +141,7 @@ let private_poly_univs =
   in
   fun () -> !b
 
-let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
+let close_proof ~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
@@ -150,7 +150,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     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
+  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. *)
@@ -160,69 +160,100 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
   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)
+  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
-       fun t p -> Future.split2 (Future.chain p (make_body t))
+      (udecl, typ), ((body, ubody), eff)
     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)
+      (* 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
+  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
+  in
+  let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in
+  { name; entries; uctx; udecl }
+
+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
+
+  (* We don't allow poly = true in this path *)
+  if poly then
+    CErrors.anomaly (Pp.str "Cannot delay universe-polymorphic constants.");
+
+  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 = 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 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
@@ -271,10 +302,10 @@ let return_proof ?(allow_partial=false) ps =
     proofs, Evd.evar_universe_context evd
 
 let close_future_proof ~opaque ~feedback_id ps proof =
-  close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof ps
+  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 ~now:true
+  close_proof ~opaque ~keep_body_ucst_separate
     (Future.from_val ~fix_exn (return_proof ps)) ps
 
 let update_global_env =
-- 
cgit v1.2.3


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.
---
 plugins/funind/gen_principle.ml |   2 +-
 stm/stm.ml                      |  10 ++--
 tactics/declare.ml              |  10 ++--
 tactics/declare.mli             |   5 ++
 tactics/pfedit.ml               |   2 +-
 tactics/proof_global.ml         | 111 ++++++++++++++++++----------------------
 tactics/proof_global.mli        |   2 +-
 vernac/lemmas.ml                |   2 +-
 vernac/vernacstate.ml           |   4 +-
 vernac/vernacstate.mli          |   2 +-
 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
-- 
cgit v1.2.3


From e9c05828bba7ceb696a5c17457b8e0826bbd94f1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 26 Mar 2020 02:45:47 -0400
Subject: [proof] Split return_proof in partial and regular versions.

This is a small refactoring as these two functions behave very
differently and the invariants are quite different, in fact regular
`return_proof` should not be exported but be part of close proof, but
there is small use in the STM still.
---
 stm/stm.ml               |  4 +--
 tactics/proof_global.ml  | 76 +++++++++++++++++++++++-------------------------
 tactics/proof_global.mli |  9 ++++--
 vernac/vernacstate.ml    |  3 +-
 vernac/vernacstate.mli   |  3 +-
 5 files changed, 49 insertions(+), 46 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index ba8eba0eed..c1156b9afe 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)
 
@@ -1661,7 +1661,7 @@ 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
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 8d62d1635d..8597d1ab09 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -141,8 +141,35 @@ let private_poly_univs =
   in
   fun () -> !b
 
-let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id
-                ((elist, uctx) : closed_proof_output) ps =
+(* 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
+  let eff = Evd.eval_side_effects evd in
+  let evd = Evd.minimize_universes evd in
+  let proof_opt c =
+    match EConstr.to_constr_opt evd c with
+    | Some p -> p
+    | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain")
+  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... *)
+  (* EJGA: actually side-effects de-duplication and this codepath is
+     unrelated. Duplicated side-effects arise from incorrect scheme
+     generation code, the main bulk of it was mostly fixed by #9836
+     but duplication can still happen because of rewriting schemes I
+     think; however the code below is mostly untested, the only
+     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 *)
+  (* 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
@@ -200,7 +227,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id
   let entry_fn p (_, t) =
     let t = EConstr.Unsafe.to_constr t in
     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
+    Declare.definition_entry ~opaque ?section_vars ~univs ~univc ~types:typ ~eff body
   in
   let entries = CList.map2 entry_fn elist (Proofview.initial_goals entry) in
   { name; entries; uctx }
@@ -254,48 +281,19 @@ let close_proof_delayed ~opaque ~keep_body_ucst_separate ?feedback_id
   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
+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
- end else
-  let Proof.{name=pid;entry} = Proof.data proof in
-  let initial_goals = Proofview.initial_goals entry in
-  let evd = Proof.return ~pid proof in
-  let eff = Evd.eval_side_effects evd in
-  let evd = Evd.minimize_universes evd in
-  let proof_opt c =
-    match EConstr.to_constr_opt evd c with
-    | Some p -> p
-    | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain")
-  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... *)
-  (* EJGA: actually side-effects de-duplication and this codepath is
-     unrelated. Duplicated side-effects arise from incorrect scheme
-     generation code, the main bulk of it was mostly fixed by #9836
-     but duplication can still happen because of rewriting schemes I
-     think; however the code below is mostly untested, the only
-     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
+ let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
+ proofs, Evd.evar_universe_context evd
 
 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 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 44b78ee911..339a7f1898 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -75,9 +75,12 @@ val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> t -> pr
 
 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
+(** 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 : opaque:opacity_flag -> feedback_id:Stateid.t -> t ->
   closed_proof_output Future.computation -> proof_object
 
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 7c191a1f86..b722acd1ad 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -164,7 +164,8 @@ 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,
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 2c9c7ecc6f..b6b24c9275 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -65,7 +65,8 @@ 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
 
-- 
cgit v1.2.3


From d9ed86ad133b48c948ea2db0bce7f00f47705970 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 26 Mar 2020 03:09:51 -0400
Subject: [proof] Minor refactorings in Proof_global

We do some minor refactoring, removing one-use local definitions, and
cleaning up the `EConstr.t -> Constr.t` path, what is going on with
the use of unsafe it now becomes clear.
---
 tactics/proof_global.ml | 54 +++++++++++++++++++++++--------------------------
 1 file changed, 25 insertions(+), 29 deletions(-)

diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 8597d1ab09..725c9ac208 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -171,38 +171,40 @@ let return_proof { proof } =
 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 { 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
+
   (* 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_body typ (c, eff) :
+  let make_body typ (body, 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
+    (* 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 ctx = constrain_variables uctx 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 ctx_body = UState.restrict ctx used_univs in
-        let univs = UState.check_mono_univ_decl ctx_body udecl in
-        utyp, univs
+        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
@@ -225,7 +227,6 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
     (typ, utyp), ((body, ubody), eff)
   in
   let entry_fn p (_, t) =
-    let t = EConstr.Unsafe.to_constr t in
     let (typ, univs), ((body,univc),eff) = make_body t p in
     Declare.definition_entry ~opaque ?section_vars ~univs ~univc ~types:typ ~eff body
   in
@@ -235,51 +236,47 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
 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; sigma } = 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
     CErrors.anomaly (Pp.str "Cannot delay universe-polymorphic constants.");
 
   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 = initial_euctx in
+  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 uctx) in
+  let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst initial_euctx) in
 
-  let make_body t p =
+  let make_body typ 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
-    (t, univctx),
+    let univctx = UState.univ_entry ~poly:false initial_euctx in
+    let typ = nf (EConstr.Unsafe.to_constr typ) in
+
+    (typ, 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
            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 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 t)
+            (Vars.universes_of_constr typ)
             (Vars.universes_of_constr pt)
         in
-        let univs = UState.restrict univs used_univs in
+        let univs = UState.restrict uctx 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 (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 }
+  { name; entries; uctx = initial_euctx }
 
 let return_partial_proof { proof } =
  let proofs = Proof.partial_proof proof in
@@ -294,7 +291,6 @@ let return_partial_proof { proof } =
 let close_future_proof ~opaque ~feedback_id ps proof =
   close_proof_delayed ~opaque ~keep_body_ucst_separate:true ~feedback_id proof ps
 
-
 let update_global_env =
   map_proof (fun p ->
       let { Proof.sigma } = Proof.data p in
-- 
cgit v1.2.3


From dc5f5f911177bc3bee518f1557b7665bc0e06d5a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 26 Mar 2020 03:18:18 -0400
Subject: [proof] Remove internal wrapper in Proof_global

After the last refactoring commit, the entry_fn function is redundant
and we can just get rid of it and get a more direct code.
---
 tactics/proof_global.ml | 34 ++++++++++++----------------------
 1 file changed, 12 insertions(+), 22 deletions(-)

diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 725c9ac208..bbf1d0d019 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -180,9 +180,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
   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 typ (body, eff) :
-    Constr.types Entries.in_universes_entry * Evd.side_effects Entries.proof_output =
-
+  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))
@@ -224,13 +222,9 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
         let utyp = UState.check_univ_decl ~poly ctx udecl in
         utyp, Univ.ContextSet.empty
     in
-    (typ, utyp), ((body, ubody), eff)
-  in
-  let entry_fn p (_, t) =
-    let (typ, univs), ((body,univc),eff) = make_body t p in
-    Declare.definition_entry ~opaque ?section_vars ~univs ~univc ~types:typ ~eff body
+    Declare.definition_entry ~opaque ?section_vars ~univs:utyp ~univc:ubody ~types:typ ~eff body
   in
-  let entries = CList.map2 entry_fn elist (Proofview.initial_goals entry) in
+  let entries = CList.map2 make_entry elist (Proofview.initial_goals entry) in
   { name; entries; uctx }
 
 let close_proof_delayed ~opaque ~keep_body_ucst_separate ?feedback_id
@@ -250,32 +244,28 @@ let close_proof_delayed ~opaque ~keep_body_ucst_separate ?feedback_id
   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
 
-  let make_body typ p =
+  let make_entry p (_, types) =
     (* Already checked the univ_decl for the type universes when starting the proof. *)
-    let univctx = UState.univ_entry ~poly:false initial_euctx in
-    let typ = nf (EConstr.Unsafe.to_constr typ) in
+    let univs = UState.univ_entry ~poly:false initial_euctx in
+    let types = nf (EConstr.Unsafe.to_constr types) in
 
-    (typ, 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
-           the declaration as well. If the declaration is non-extensible,
-           this will prevent the body from adding universes and constraints. *)
+             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 typ)
+            (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 entry_fn p (_, t) =
-    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
+  let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in
   { name; entries; uctx = initial_euctx }
 
 let return_partial_proof { proof } =
-- 
cgit v1.2.3


From 49b559ccb6d17b5356bc0e43c81a8363ec0b4768 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 26 Mar 2020 03:21:18 -0400
Subject: [proof] Fixme on unused return type.

---
 tactics/proof_global.ml  | 3 +--
 tactics/proof_global.mli | 5 ++---
 2 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index bbf1d0d019..fe2f828fb4 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
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index 339a7f1898..59881dffa1 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -94,7 +94,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
-- 
cgit v1.2.3


From 7a2e41abd8559d0bd4683e513dcb0b83987a9128 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 26 Mar 2020 15:36:33 -0400
Subject: [proof] Remove unused parameter in the delayed save path.

---
 tactics/proof_global.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index fe2f828fb4..7d86c6a1d1 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -226,8 +226,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
   let entries = CList.map2 make_entry 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 close_proof_delayed ~opaque ?feedback_id (fpl : closed_proof_output Future.computation) ps =
   let { section_vars; proof; udecl; initial_euctx } = ps in
   let { Proof.name; poly; entry; sigma } = Proof.data proof in
 
@@ -278,7 +277,7 @@ let return_partial_proof { proof } =
  proofs, Evd.evar_universe_context evd
 
 let close_future_proof ~opaque ~feedback_id ps proof =
-  close_proof_delayed ~opaque ~keep_body_ucst_separate:true ~feedback_id proof ps
+  close_proof_delayed ~opaque ~feedback_id proof ps
 
 let update_global_env =
   map_proof (fun p ->
-- 
cgit v1.2.3


From 0eadf776ba78dcfdcab842f38f5de871ed337376 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 26 Mar 2020 17:04:16 -0400
Subject: [proof] [stm] Force `opaque` in `close_future_proof`

Following an observation by Enrico Tassi, we remove the `opaque`
parameter from `close_future_proof`, it should never be called with
transparent constants.

We will enforce this thru typing at the proof layer soon.
---
 stm/stm.ml               | 14 +++++++-------
 tactics/proof_global.ml  | 13 +++++++------
 tactics/proof_global.mli |  3 +--
 vernac/vernacstate.ml    |  4 ++--
 vernac/vernacstate.mli   |  1 -
 5 files changed, 17 insertions(+), 18 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index c1156b9afe..5b88ee3d68 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -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);
@@ -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
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 7d86c6a1d1..d7f4cb3b9a 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -226,7 +226,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
   let entries = CList.map2 make_entry elist (Proofview.initial_goals entry) in
   { name; entries; uctx }
 
-let close_proof_delayed ~opaque ?feedback_id (fpl : closed_proof_output Future.computation) ps =
+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
 
@@ -234,7 +234,6 @@ let close_proof_delayed ~opaque ?feedback_id (fpl : closed_proof_output Future.c
   if poly then
     CErrors.anomaly (Pp.str "Cannot delay universe-polymorphic constants.");
 
-  let opaque = match opaque with Opaque -> true | Transparent -> false in
   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
@@ -242,6 +241,9 @@ let close_proof_delayed ~opaque ?feedback_id (fpl : closed_proof_output Future.c
   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
@@ -261,11 +263,13 @@ let close_proof_delayed ~opaque ?feedback_id (fpl : closed_proof_output Future.c
         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
+    |> 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
@@ -276,9 +280,6 @@ let return_partial_proof { proof } =
  let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
  proofs, Evd.evar_universe_context evd
 
-let close_future_proof ~opaque ~feedback_id ps proof =
-  close_proof_delayed ~opaque ~feedback_id proof ps
-
 let update_global_env =
   map_proof (fun p ->
       let { Proof.sigma } = Proof.data p in
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index 59881dffa1..874708ded8 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -81,8 +81,7 @@ 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 : opaque:opacity_flag -> feedback_id:Stateid.t -> t ->
-  closed_proof_output Future.computation -> proof_object
+val close_future_proof : feedback_id:Stateid.t -> t -> closed_proof_output Future.computation -> proof_object
 
 val get_open_goals : t -> int
 
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index b722acd1ad..a4e9c8e1ab 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -167,8 +167,8 @@ module Proof_global = struct
   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 =
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index b6b24c9275..9c4de7720c 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -71,7 +71,6 @@ module Proof_global : sig
   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
 
-- 
cgit v1.2.3


From 7afd5e9fb7ba9e5fc41e41fd54eb90ee8cb13993 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 30 Mar 2020 18:58:24 -0400
Subject: [proof] Improve comment and argument name.

As suggested by Gaëtan Gilbert.
---
 tactics/declare.ml      | 4 ++--
 tactics/declare.mli     | 6 +++---
 tactics/proof_global.ml | 2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/tactics/declare.ml b/tactics/declare.ml
index a149850a64..324007930a 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -188,8 +188,8 @@ 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) ?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);
+    ?(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;
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 6ea08d5b0e..615cffeae7 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -64,9 +64,9 @@ val definition_entry
   -> ?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 *)
+  -> ?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/proof_global.ml b/tactics/proof_global.ml
index d7f4cb3b9a..d7dcc13e79 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -221,7 +221,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
         let utyp = UState.check_univ_decl ~poly ctx udecl in
         utyp, Univ.ContextSet.empty
     in
-    Declare.definition_entry ~opaque ?section_vars ~univs:utyp ~univc:ubody ~types:typ ~eff body
+    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 }
-- 
cgit v1.2.3