PREREQUISITES ------------- This version is known to compile with: - Coq 8.4pl1 - SCons 2.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:swasey/coq-stdpp.git" did not exist on "3503a91f8c85b2a01a73ec5fea43cc67ee6c4006"
Forked from
Iris / stdpp
2758 commits behind the upstream repository.
Robbert Krebbers
authored
Major changes: * Make void a base type, and include a proper void base value. This is necessary because expressions (free, functions without return value) can yield a void. We now also allow void casts conforming to the C standard. * Various missing lemmas about typing, weakening, decidability, ... * The operations "free" and "alloc" now operate on l-values instead of r-values. This removes some duplication. * Improve notations of expressions and statements. Change the presence of the operators conforming to the C standard. Small changes: * Use the classes "Typed" and "TypeCheck" for validity of indexes in memory. This gives more uniform notations. * New tactic "typed_inversion" performs inversion on an inductive predicate of type "Typed" and folds the premises. * Remove a horrible hack in the definitions of the classes "FMap", "MBind", "OMap", "Alter" that was used to let "simpl" behave better. Instead, we have defined a tactic "csimpl" that folds the results after performing an ordinary "simpl". * Fast operation to remove duplicates from lists using hashsets. * Make various type constructors (mainly finite map implementations) universe polymorphic by packing them into an inductive. This way, the whole C syntax can live in type, avoiding the need for (slow) universe checks.