aboutsummaryrefslogtreecommitdiffstats
path: root/ia32/SelectOpproof.v
Commit message (Expand)AuthorAgeFilesLines
* Take advantage of Cmaskzero and Cmasknotzero.xleroy2012-02-241-0/+23
* Merge of the "volatile" branch:xleroy2012-02-041-0/+25
* Merge of the nonstrict-ops branch:xleroy2012-01-141-676/+460
* Merge of branch "unsigned-offsets":xleroy2011-04-091-35/+39
* float->int conversions, continued: weaker axiomatization.xleroy2010-10-291-2/+2
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-281-9/+17
* Merge of the reuse-temps branch:xleroy2010-09-021-0/+935