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 /checker/check.ml | |
| 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 'checker/check.ml')
| -rw-r--r-- | checker/check.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/check.ml b/checker/check.ml index a2c8a0f25d..cc5ad0af4c 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -50,7 +50,7 @@ let pr_path sp = type compilation_unit_name = DirPath.t -type seg_proofs = Constr.constr Future.computation array +type seg_proofs = Constr.constr option array type library_t = { library_name : compilation_unit_name; |