aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-05-20 11:51:31 +0200
committerPierre-Marie Pédrot2019-05-24 09:00:10 +0200
commitb245a6c46bc3ef70142e8a165f6cde54265b941e (patch)
treef042b65df5510e2a1551c5ffb33b5c1cc64f5d0d /kernel/nativelambda.mli
parentca4b15c2ba733bdff783762bbfc4b53f88014320 (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/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions