diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-05-16 20:17:18 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-05-16 20:20:25 +0200 |
commit | c4bdf93e358b97b32e0d80d6c7d1b79a2ece1dc2 (patch) | |
tree | cd743dccec87bd991df8cc9944db902d7a546ed5 /lib/future.mli | |
parent | d483b7171dafadbe01520bbb6d0c75aa0d6099a7 (diff) |
Decent error message when a constant is not found
Diffstat (limited to 'lib/future.mli')
0 files changed, 0 insertions, 0 deletions