summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-07-31 07:33:53 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-07-31 07:33:53 +0000
commitf2d0caa5f7594cf936713f3bd6cdc3ab5a6f9626 (patch)
tree2aa5893447519500da5b41b97c8c767b259b9b34 /doc
parent769589fb4f72edf46c16a396de6777d8e2fbb9bf (diff)
Add Mem.free_parallel_inject and use it to simplify Events a bit.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2556 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions