Make [Proof_global.closed_proof_output] opaque

This means return_proof is the only place where it can be produced.

We need to change the stm a bit as it keeps a pointer to a
[closed_proof_output] to join and to check if it failed, and it needs
a way to create a dummy in 1 case.

I'm not sure if this works correctly though, how to test?

We also inline the used bits of [return_proof ~allow_partial:true] in
[save_lemma_admitted] to get [Proof using] info. We could
alternatively expose the [closed_proof_output -> constr list]
projection. I think the code is easier to understand this way though,
as we don't have to read [return_proof] and figure out that the side
effect manipulation is ignored etc.

Note that the "this will warn" comment was outdated since
73daf37ccc7a44cd29c9b67405111756c75cb26a

3 files changed, 14 insertions, 14 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 2b68e1778d..eff2403eca 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -170,7 +170,7 @@ type fork_t = aast * Vcs_.Branch.t * opacity_guarantee * Names.Id.t list
 type qed_t = {
   qast : aast;
   keep : vernac_qed_type;
-  mutable fproof : (future_proof * AsyncTaskQueue.cancel_switch) option;
+  mutable fproof : (future_proof option * AsyncTaskQueue.cancel_switch) option;
   brname : Vcs_.Branch.t;
   brinfo : branch_type Vcs_.branch_info
 }
@@ -2460,8 +2460,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                     let fp, cancel =
                       Slaves.build_proof ~doc
                         ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name in
-                    Future.replace ofp fp;
-                    qed.fproof <- Some (fp, cancel);
+                    Future.replace (Option.get ofp) fp;
+                    qed.fproof <- Some (Some fp, cancel);
                     (* We don't generate a new state, but we still need
                      * to install the right one *)
                     State.install_cached id
@@ -2476,7 +2476,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                         ProofTask.build_proof_here ~doc ?loc
                           ~drop_pt exn_info block_stop, ref false
                     in
-                    qed.fproof <- Some (fp, cancel);
+                    qed.fproof <- Some (Some fp, cancel);
                     let opaque = match keep' with
                       | VtKeepAxiom | VtKeepOpaque ->
                         Proof_global.Opaque (* Admitted -> Opaque should be OK. *)
@@ -2510,9 +2510,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                   match keep with
                   | VtDrop -> None
                   | VtKeep VtKeepAxiom ->
-                      let ctx = UState.empty in
-                      let fp = Future.from_val ([],ctx) in
-                      qed.fproof <- Some (fp, ref false); None
+                      qed.fproof <- Some (None, ref false); None
                   | VtKeep opaque ->
                     let opaque = let open Proof_global in  match opaque with
                       | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent
@@ -2709,7 +2707,7 @@ let rec join_admitted_proofs id =
   let view = VCS.visit id in
   match view.step with
   | `Qed ({ keep = VtKeep VtKeepAxiom; fproof = Some (fp,_) },_) ->
-       ignore(Future.force fp);
+       Option.iter (fun fp -> ignore(Future.force fp)) fp;
        join_admitted_proofs view.next
   | _ -> join_admitted_proofs view.next
 
@@ -3114,7 +3112,7 @@ let edit_at ~doc id =
       (VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in
   let has_failed qed_id =
     match VCS.visit qed_id with
-    | { step = `Qed ({ fproof = Some (fp,_) }, _) } -> Future.is_exn fp
+    | { step = `Qed ({ fproof = Some (Some fp,_) }, _) } -> Future.is_exn fp
     | _ -> false in
   let rec master_for_br root tip =
       if Stateid.equal tip Stateid.initial then tip else
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index b9d1b37a11..9161eae82f 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -79,7 +79,7 @@ val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.
  * Both access the current proof state. The former is supposed to be
  * chained with a computation that completed the proof *)
 
-type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
+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. *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index cf322c52d0..865eded545 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -295,16 +295,18 @@ let save_lemma_admitted ~(lemma : t) : unit =
     | _ -> CErrors.anomaly ~label:"Lemmas.save_proof" (Pp.str "more than one statement.")
   in
   let typ = EConstr.Unsafe.to_constr typ in
-  (* This will warn if the proof is complete *)
-  let pproofs, _univs = Proof_global.return_proof ~allow_partial:true lemma.proof in
+  let proof = Proof_global.get_proof lemma.proof in
+  let pproofs = Proof.partial_proof proof in
   let sec_vars =
     if not (get_keep_admitted_vars ()) then None
     else match Proof_global.get_used_variables lemma.proof, pproofs with
       | Some _ as x, _ -> x
-      | None, (pproof, _) :: _ ->
+      | None, pproof :: _ ->
         let env = Global.env () in
         let ids_typ = Environ.global_vars_set env typ in
-        let ids_def = Environ.global_vars_set env pproof in
+        (* [pproof] is evar-normalized by [partial_proof]. We don't
+           count variables appearing only in the type of evars. *)
+        let ids_def = Environ.global_vars_set env (EConstr.Unsafe.to_constr pproof) in
         Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
       | _ -> None in
   let universes = Proof_global.get_initial_euctx lemma.proof in