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
"git-rts@gitlab.mpi-sws.org:simonspies/stdpp.git" did not exist on "26917d003249dcb1a379fc6c5edddefbb5a4ac4a"
Forked from
Iris / stdpp
2717 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.