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 /vernac/declare.mli | |
| 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 'vernac/declare.mli')
| -rw-r--r-- | vernac/declare.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/vernac/declare.mli b/vernac/declare.mli index 0520bf8717..2d8e9656b1 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -280,9 +280,10 @@ module Proof : sig (* 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 - (* Make a dummy value, used in the stm *) - val default : unit -> t end val info : t -> Proof_info.t |