-
- Downloads
- Proofmode for rust_lang (TODO : CAS, Free, Fork?, Skip?, memcpy)
+ Put laters around heap assumptions in heap.v - A few fixes in substitutions.v : + Replaced csimpl by cbn [subst_l subst'] in simpl_subst for better performances + Enforce the right order for rewriting do_subst + added list constructors instances for WSubstL + Fixed the hint extern for WSubst Rec - Compatibility with new intro patterns - Better notations for language constructs : function parameters are listed within [] - Proved memcpy. TODO : improve perforamnces (time and memory).
Showing
- _CoqProject 8 additions, 5 deletions_CoqProject
- derived.v 2 additions, 2 deletionsderived.v
- heap.v 63 additions, 52 deletionsheap.v
- lifting.v 23 additions, 23 deletionslifting.v
- memcpy.v 31 additions, 0 deletionsmemcpy.v
- notation.v 28 additions, 7 deletionsnotation.v
- proofmode.v 145 additions, 0 deletionsproofmode.v
- substitution.v 13 additions, 3 deletionssubstitution.v
- tactics.v 3 additions, 3 deletionstactics.v
- wp_tactics.v 125 additions, 0 deletionswp_tactics.v
Loading
Please register or sign in to comment