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

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