diff options
| author | Pierre-Marie Pédrot | 2019-05-20 11:51:31 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-24 09:00:10 +0200 |
| commit | b245a6c46bc3ef70142e8a165f6cde54265b941e (patch) | |
| tree | f042b65df5510e2a1551c5ffb33b5c1cc64f5d0d /kernel/opaqueproof.mli | |
| parent | ca4b15c2ba733bdff783762bbfc4b53f88014320 (diff) | |
Statically ensure the content of delayed proofs in vio file.
Before, we would store futures, but it was actually ensured by the
upper layers that they were either evaluated or stored by the STM
somewhere else. We simply replace this type with an option, thus
removing the Future.computation type from vo/vio files.
This also enhances debug printing, as the latter is unable to properly
print futures.
Diffstat (limited to 'kernel/opaqueproof.mli')
| -rw-r--r-- | kernel/opaqueproof.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index b84aeaf35a..3b61ec71ef 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -59,9 +59,9 @@ val discharge_direct_opaque : val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit -val dump : opaquetab -> - Constr.t Future.computation array * - Univ.ContextSet.t Future.computation array * +val dump : ?except:Future.UUIDSet.t -> opaquetab -> + Constr.t option array * + Univ.ContextSet.t option array * cooking_info list array * int Future.UUIDMap.t @@ -73,7 +73,7 @@ val dump : opaquetab -> *) val set_indirect_opaque_accessor : - (DirPath.t -> int -> constr Future.computation) -> unit + (DirPath.t -> int -> constr option) -> unit val set_indirect_univ_accessor : - (DirPath.t -> int -> Univ.ContextSet.t Future.computation option) -> unit + (DirPath.t -> int -> Univ.ContextSet.t option) -> unit |