Skip to content
Snippets Groups Projects
Forked from Iris / stdpp
2726 commits behind the upstream repository.
user avatar
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.
c5c0d373
History
Name Last commit Last update
theories
README
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