PREREQUISITES ------------- This version is known to compile with: - Coq 8.4pl3 - SCons 2.0 - Ocaml 4.01.0 BUILDING INSTRUCTIONS --------------------- Say "scons" to build the full library, or "scons some_module.vo" to just build some_module.vo (and its dependencies). In addition to common Make options like -j N and -k, SCons supports some useful options of its own, such as --debug=time, which displays the time spent executing individual build commands. scons -c replaces Make clean
Forked from
Iris / stdpp
2726 commits behind the upstream repository.
Robbert Krebbers
authored
Memory refinements now carry a boolean parameter that has the following meaning: [false] : Behave like a simple renaming of memories that merely allows to permute object identifiers. It does not allow to refine memories into a more defined version. [true] : Behave like before. Objects can be injected, and memory contents can be refined into a more defined variant. We make refinements parametric in these two variant to avoid code duplication, and because the [false] variant is a special case of the [true] variant. For completeness of the executable semantics, we now use the [false] variant.