aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/future.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-05-16 20:17:18 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-05-16 20:20:25 +0200
commitc4bdf93e358b97b32e0d80d6c7d1b79a2ece1dc2 (patch)
treecd743dccec87bd991df8cc9944db902d7a546ed5 /lib/future.mli
parentd483b7171dafadbe01520bbb6d0c75aa0d6099a7 (diff)
Decent error message when a constant is not found
Diffstat (limited to 'lib/future.mli')
0 files changed, 0 insertions, 0 deletions