aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Op.v
Commit message (Expand)AuthorAgeFilesLines
* Merge of the reuse-temps branch:xleroy2010-09-021-15/+75
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-26/+15
* 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