diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-03-06 09:33:39 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-03-06 09:33:39 +0100 |
| commit | 69726a600dc4277d562193253b5a8e76f0a474eb (patch) | |
| tree | fb9c449a0e21b4df9b102955a85e1bb2f003593b /common/Linking.v | |
| parent | 0507fa6e0a242b58d90037ef0177ec85649e3f11 (diff) | |
| download | compcert-kvx-69726a600dc4277d562193253b5a8e76f0a474eb.tar.gz compcert-kvx-69726a600dc4277d562193253b5a8e76f0a474eb.zip | |
Preliminaries: minor extensions to Memory
- Make Mem.unchanged_on transitive.
- Add Mem.drop_perm_unchanged_on.
Diffstat (limited to 'common/Linking.v')
0 files changed, 0 insertions, 0 deletions