diff options
| author | gareuselesinge | 2013-08-08 18:50:36 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-08-08 18:50:36 +0000 |
| commit | 0faf3c5a53113ec8f31c1747c9cafe4118831282 (patch) | |
| tree | 3f1ce67417414609ad45b82fa3e38771bb108528 /lib/errors.ml | |
| parent | 6df91acf9e7d61d3a0df86bdf4c4c67de4c4ae9c (diff) | |
Future library to represent pure computations
Since the whole system is imperative, futures are run protecting
the global state, and the final state is also saved to let the user
freely chain futures.
Futures can represent local (lazy) computations or remote ones
(delegated). Delegating a future lets a third party assign its
value at some poit in the future; in the meanwhile accessing the
future value raises an exception.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16669 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/errors.ml')
0 files changed, 0 insertions, 0 deletions