aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Op.v
Commit message (Expand)AuthorAgeFilesLines
...
* 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-12/+12
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-118/+46
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-0/+925