aboutsummaryrefslogtreecommitdiffstats
path: root/arm/Op.v
Commit message (Expand)AuthorAgeFilesLines
* Updating ARM portxleroy2010-03-281-2/+1
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-13/+13
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-191-20/+20
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-14/+14
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-112/+26
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-0/+1007