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

0 files changed, 0 insertions, 0 deletions