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
2693 commits behind the upstream repository.
Robbert Krebbers
authored
The refinement relation on addresses allows union references to be refined: (β2 → β1) → RUnion i s β1 ⊆ RUnion i s β2 The result is that frozen values are below their unfrozen variant, which made it possible to prove that constant propagation (see constant_propagation.v) can be performed on the level of the memory model.