diff options
| author | Emilio Jesus Gallego Arias | 2020-11-19 19:14:59 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-20 02:32:44 +0100 |
| commit | 36aeb43062aa6671020457538577311fbe7d7b3a (patch) | |
| tree | f85a406a2eec4816acd47a22f0e609be73b670e4 /stm | |
| parent | 3037172c80190b74b2c0f3017420cc871e74c996 (diff) | |
[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`.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 8 |
1 files changed, 2 insertions, 6 deletions
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 *) |