diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-31 07:33:53 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-31 07:33:53 +0000 |
| commit | f2d0caa5f7594cf936713f3bd6cdc3ab5a6f9626 (patch) | |
| tree | 2aa5893447519500da5b41b97c8c767b259b9b34 /flocq/Appli/Fappli_IEEE.v | |
| parent | 769589fb4f72edf46c16a396de6777d8e2fbb9bf (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 'flocq/Appli/Fappli_IEEE.v')
0 files changed, 0 insertions, 0 deletions