aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-18 13:52:06 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-18 13:52:06 +0000
commit27bbbdc0ef930b1efca7b268e859d4e93927b365 (patch)
tree6632f836948e473649347a2919bbc4c678d96592 /checker
parentc44067d1565e7c139c9bde4d041661ac256c3869 (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')
-rw-r--r--checker/check.mllib1
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