From 36aeb43062aa6671020457538577311fbe7d7b3a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 19 Nov 2020 19:14:59 +0100
Subject: [stm] [declare] Try to propagate safe bits of proof information

Since 8.5, the STM could not delegate proof information it was
contained inside a closure. This could potentially create some
problems, as witnessed in #12586.

Recent refactoring have reified however much of this state, so it
seems a good idea to use bits of the state now, at the cost of
introducing some safeguards in `declare.ml` w.r.t. `Ephemerons`.
---
 stm/stm.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index df7e35beb5..977b814e93 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1470,14 +1470,13 @@ end = struct (* {{{ *)
         (* Unfortunately close_future_proof and friends are not pure so we need
            to set the state manually here *)
           State.unfreeze st;
-          let pobject, _info =
+          let pobject, pinfo =
             PG_compat.close_future_proof ~feedback_id:stop (Future.from_val proof) in
 
           let st = Vernacstate.freeze_interp_state ~marshallable:false in
           let opaque = Opaque in
           try
             let _pstate =
-              let pinfo = Declare.Proof.Proof_info.default () in
               stm_qed_delay_proof ~st ~id:stop
                 ~proof:pobject ~pinfo ~loc ~control:[] (Proved (opaque,None)) in
             ()
@@ -1621,12 +1620,9 @@ end = struct (* {{{ *)
       else begin
       let opaque = Opaque in
 
-      (* The original terminator, a hook, has not been saved in the .vio*)
-      let proof, _info =
+      let proof, pinfo =
         PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true in
 
-      let pinfo = Declare.Proof.Proof_info.default () in
-
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
 
-- 
cgit v1.2.3