diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-06-23 22:54:22 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-06-23 22:54:38 +0200 |
| commit | a2fa3dd1ec96cd70c817ff375d7b857924bb9825 (patch) | |
| tree | 8d4a5d14ea27fd8325d6d74d0fcc269a0fc46a72 /library/library.mli | |
| parent | 1834d60f373fb63c32d179f2cf03ee4da7880bb0 (diff) | |
obligations: wrap Ephemeron.get to make error more informative
A worker should never have to access the still-to-be-proved
obligations. If that happens, raise an informative anomaly.
Diffstat (limited to 'library/library.mli')
0 files changed, 0 insertions, 0 deletions