diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-18 13:52:06 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-18 13:52:06 +0000 |
| commit | 27bbbdc0ef930b1efca7b268e859d4e93927b365 (patch) | |
| tree | 6632f836948e473649347a2919bbc4c678d96592 /checker/check.mllib | |
| parent | c44067d1565e7c139c9bde4d041661ac256c3869 (diff) | |
Ephemeron: marshaling friendly keys
Ideally all unmarshallable content in the state should be
stocked using Ephemeron keys. In this way the state becomes
always marshallable (because the unmarshallable content is magically
dropped). The mli contains more detailed doc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16891 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/check.mllib')
| -rw-r--r-- | checker/check.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index 759be8729..08196d27f 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -23,6 +23,7 @@ CString CArray CStack Util +Ephemeron Future CUnix System |