diff options
| author | Pierre-Marie Pédrot | 2019-05-20 11:30:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-24 09:00:10 +0200 |
| commit | ca4b15c2ba733bdff783762bbfc4b53f88014320 (patch) | |
| tree | 6e4ee88413dc99d34c563ecdcac165d18920dd91 /checker/values.ml | |
| parent | 26169d33b45aae8bf2dfafa2b400a9780c73ea13 (diff) | |
Remove a useless call to the Future API for opaque proofs in the STM.
We know statically that the check function producing this forces its
argument, so there is no point in chaining futures lazily.
Diffstat (limited to 'checker/values.ml')
0 files changed, 0 insertions, 0 deletions