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 /dev | |
| 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 'dev')
| -rw-r--r-- | dev/printers.mllib | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index c3d3ce7091..37ee00517d 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -35,6 +35,8 @@ Rtree Heap Dnet Genarg +Stateid +Future Names Univ @@ -49,6 +51,7 @@ Cbytecodes Copcodes Cemitcodes Nativevalues +Future Lazyconstr Declareops Retroknowledge |