aboutsummaryrefslogtreecommitdiffstats
path: root/common/Memory.v
Commit message (Expand)AuthorAgeFilesLines
...
* Cleaned up old commented-out partsxleroy2011-08-191-10/+0
* Back from Oregon commit. xleroy2011-07-051-19/+670
* Merge of branch "unsigned-offsets":xleroy2011-04-091-33/+34
* Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.xleroy2011-03-091-6/+6
* Memory.v: added drop_perm operationxleroy2010-09-211-22/+315
* Render unto Caesar... (Mention contribution by Dockins and Steward.)xleroy2010-07-081-0/+2
* Support for inlined built-ins.xleroy2010-06-291-66/+64
* Merging the Princeton implementation of the memory model. Separate axioms in...xleroy2010-06-281-260/+498
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-0/+2844