aboutsummaryrefslogtreecommitdiffstats
path: root/arm/SelectOp.v
Commit message (Collapse)AuthorAgeFilesLines
* Declaration of use_fused_mul, unused in this port but needed for extraction ↵xleroy2009-08-181-0/+4
| | | | | | (I think) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1131 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Refactored Selection.v and Selectionproof.v into a machine-dependent part + ↵xleroy2009-08-171-0/+1195
a machine-independent part. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e