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 /kernel/safe_typing.mli | |
| 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 'kernel/safe_typing.mli')
0 files changed, 0 insertions, 0 deletions