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

1 files changed, 7 insertions, 9 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