[stm] [declare] Remove pinfo internals hack.

After the previous commit, the stm should correctly pass proof
information, thus we make `proof_object` carry it removing a bunch of
internal code.

6 files changed, 28 insertions, 54 deletions

diff --git a/vernac/declare.ml b/vernac/declare.ml
index a7d9a604b1..73ebca276d 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1369,11 +1369,6 @@ module Proof_info = struct
     ; proof_ending = CEphemeron.create proof_ending
     }
 
-  (* This is used due to a deficiency on the API, should fix *)
-  let add_first_thm ~pinfo ~name ~typ ~impargs =
-    let cinfo : Constr.t CInfo.t = CInfo.make ~name ~impargs ~typ:(EConstr.Unsafe.to_constr typ) () in
-    { pinfo with cinfo = cinfo :: pinfo.cinfo }
-
 end
 
 type t =
@@ -1387,7 +1382,6 @@ type t =
 
 (*** Proof Global manipulation ***)
 
-let info { pinfo } = pinfo
 let get ps = ps.proof
 let get_name ps = (Proof.data ps.proof).Proof.name
 let get_initial_euctx ps = ps.initial_euctx
@@ -1565,6 +1559,7 @@ type proof_object =
   (* [name] only used in the STM *)
   ; entries : Evd.side_effects proof_entry list
   ; uctx: UState.t
+  ; pinfo : Proof_info.t
   }
 
 let get_po_name { name } = name
@@ -1672,7 +1667,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
     definition_entry_core ~opaque ?using ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
   in
   let entries = CList.map make_entry elist  in
-  { name; entries; uctx }
+  { name; entries; uctx; pinfo }
 
 type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
 
@@ -1717,7 +1712,7 @@ let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.comput
     |> delayed_definition_entry ~opaque ~feedback_id ~using ~univs ~types
   in
   let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in
-  { name; entries; uctx = initial_euctx }
+  { name; entries; uctx = initial_euctx; pinfo }
 
 let close_future_proof = close_proof_delayed
 
@@ -2082,7 +2077,7 @@ let save ~pm ~proof ~opaque ~idopt =
   let proof_info = process_idopt_for_save ~idopt proof.pinfo in
   finalize_proof ~pm proof_obj proof_info
 
-let save_regular ~proof ~opaque ~idopt =
+let save_regular ~(proof : t) ~opaque ~idopt =
   let open Proof_ending in
   match CEphemeron.default proof.pinfo.Proof_info.proof_ending Regular with
   | Regular ->
@@ -2093,8 +2088,8 @@ let save_regular ~proof ~opaque ~idopt =
 (***********************************************************************)
 (* Special case to close a lemma without forcing a proof               *)
 (***********************************************************************)
-let save_lemma_admitted_delayed ~pm ~proof ~pinfo =
-  let { entries; uctx } = proof in
+let save_lemma_admitted_delayed ~pm ~proof =
+  let { entries; uctx; pinfo } = proof in
   if List.length entries <> 1 then
     CErrors.user_err Pp.(str "Admitted does not support multiple statements");
   let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
@@ -2105,17 +2100,10 @@ let save_lemma_admitted_delayed ~pm ~proof ~pinfo =
   let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
   finish_admitted ~pm ~uctx ~pinfo ~sec_vars ~univs
 
-let save_lemma_proved_delayed ~pm ~proof ~pinfo ~idopt =
-  (* vio2vo calls this but with invalid info, we have to workaround
-     that to add the name to the info structure *)
-  (* IMPORTANT: after #13425 this may not be needed. *)
-  if CList.is_empty pinfo.Proof_info.cinfo then
-    let name = get_po_name proof in
-    let info = Proof_info.add_first_thm ~pinfo ~name ~typ:EConstr.mkSet ~impargs:[] in
-    finalize_proof ~pm proof info
-  else
-    let info = process_idopt_for_save ~idopt pinfo in
-    finalize_proof ~pm proof info
+let save_lemma_proved_delayed ~pm ~proof ~idopt =
+  (* vio2vo used to call this with invalid [pinfo], now it should work fine. *)
+  let pinfo = process_idopt_for_save ~idopt proof.pinfo in
+  finalize_proof ~pm proof pinfo
 
 end (* Proof module *)
 
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 2d8e9656b1..e4c77113af 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -278,15 +278,6 @@ module Proof : sig
       environment and empty evar_map. *)
   val get_current_context : t -> Evd.evar_map * Environ.env
 
-  (* Internal, don't use *)
-  module Proof_info : sig
-    (* Note to developers, when marshalled, this will still lose some
-       fields, such as hooks or proof terminators, as they are still
-       closures. *)
-    type t
-  end
-  val info : t -> Proof_info.t
-
   (** {2 Proof delay API, warning, internal, not stable *)
 
   (* Intermediate step necessary to delegate the future.
@@ -314,13 +305,11 @@ module Proof : sig
   val save_lemma_admitted_delayed :
        pm:OblState.t
     -> proof:proof_object
-    -> pinfo:Proof_info.t
     -> OblState.t
 
   val save_lemma_proved_delayed
     : pm:OblState.t
     -> proof:proof_object
-    -> pinfo:Proof_info.t
     -> idopt:Names.lident option
     -> OblState.t * GlobRef.t list
 
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index edf48fef1a..57d9e0ac3c 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -226,24 +226,24 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) =
 *)
 
 (* Interpreting a possibly delayed proof *)
-let interp_qed_delayed ~proof ~pinfo ~st pe : Vernacstate.LemmaStack.t option * Declare.OblState.t =
+let interp_qed_delayed ~proof ~st pe : Vernacstate.LemmaStack.t option * Declare.OblState.t =
   let stack = st.Vernacstate.lemmas in
   let pm = st.Vernacstate.program in
   let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in
   let pm = match pe with
     | Admitted ->
-      Declare.Proof.save_lemma_admitted_delayed ~pm ~proof ~pinfo
+      Declare.Proof.save_lemma_admitted_delayed ~pm ~proof
     | Proved (_,idopt) ->
-      let pm, _ = Declare.Proof.save_lemma_proved_delayed ~pm ~proof ~pinfo ~idopt in
+      let pm, _ = Declare.Proof.save_lemma_proved_delayed ~pm ~proof ~idopt in
       pm
   in
   stack, pm
 
-let interp_qed_delayed_control ~proof ~pinfo ~st ~control { CAst.loc; v=pe } =
+let interp_qed_delayed_control ~proof ~st ~control { CAst.loc; v=pe } =
   let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in
   List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn)
     control
-    (fun ~st -> interp_qed_delayed ~proof ~pinfo ~st pe)
+    (fun ~st -> interp_qed_delayed ~proof ~st pe)
     ~st
 
 (* General interp with management of state *)
@@ -273,6 +273,6 @@ let interp_gen ~verbosely ~st ~interp_fn cmd =
 let interp ?(verbosely=true) ~st cmd =
   interp_gen ~verbosely ~st ~interp_fn:interp_control cmd
 
-let interp_qed_delayed_proof ~proof ~pinfo ~st ~control pe : Vernacstate.t =
+let interp_qed_delayed_proof ~proof ~st ~control pe : Vernacstate.t =
   interp_gen ~verbosely:false ~st
-    ~interp_fn:(interp_qed_delayed_control ~proof ~pinfo ~control) pe
+    ~interp_fn:(interp_qed_delayed_control ~proof ~control) pe
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 84d3256c9f..f31bebf7db 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -15,7 +15,6 @@ val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control ->
    proof and won't be forced *)
 val interp_qed_delayed_proof
   :  proof:Declare.Proof.proof_object
-  -> pinfo:Declare.Proof.Proof_info.t
   -> st:Vernacstate.t
   -> control:Vernacexpr.control_flag list
   -> Vernacexpr.proof_end CAst.t
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 204008997d..011d943c9b 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -204,18 +204,14 @@ module Declare_ = struct
       s_lemmas := Some stack;
       res
 
-  type closed_proof = Declare.Proof.proof_object * Declare.Proof.Proof_info.t
-
   let return_proof () = cc Declare.Proof.return_proof
   let return_partial_proof () = cc Declare.Proof.return_partial_proof
 
   let close_future_proof ~feedback_id pf =
-    cc (fun pt -> Declare.Proof.close_future_proof ~feedback_id pt pf,
-                  Declare.Proof.info pt)
+    cc (fun pt -> Declare.Proof.close_future_proof ~feedback_id pt pf)
 
   let close_proof ~opaque ~keep_body_ucst_separate =
-    cc (fun pt -> Declare.Proof.close_proof ~opaque ~keep_body_ucst_separate pt,
-                  Declare.Proof.info pt)
+    cc (fun pt -> Declare.Proof.close_proof ~opaque ~keep_body_ucst_separate pt)
 
   let discard_all () = s_lemmas := None
   let update_sigma_univs ugraph = dd (Declare.Proof.update_sigma_univs ugraph)
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index e1b13dcb73..e9e06e6d8e 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -104,13 +104,15 @@ module Declare : sig
   val return_proof : unit -> Declare.Proof.closed_proof_output
   val return_partial_proof : unit -> Declare.Proof.closed_proof_output
 
-  type closed_proof = Declare.Proof.proof_object * Declare.Proof.Proof_info.t
-
-  val close_future_proof :
-    feedback_id:Stateid.t ->
-    Declare.Proof.closed_proof_output Future.computation -> closed_proof
-
-  val close_proof : opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof
+  val close_future_proof
+    : feedback_id:Stateid.t
+    -> Declare.Proof.closed_proof_output Future.computation
+    -> Declare.Proof.proof_object
+
+  val close_proof
+    : opaque:Vernacexpr.opacity_flag
+    -> keep_body_ucst_separate:bool
+    -> Declare.Proof.proof_object
 
   val discard_all : unit -> unit
   val update_sigma_univs : UGraph.t -> unit