aboutsummaryrefslogtreecommitdiffstats
path: root/ia32/Asmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Merge of the nonstrict-ops branch:xleroy2012-01-141-4/+9
* More careful treatment of 'load immediate 0' as 'xor self'xleroy2011-08-181-0/+2
* Locations.v: add Loc.diff_dec.xleroy2011-08-141-3/+15
* IA32 port: more faithful treatment of pseudoregister ST0.xleroy2011-08-081-3/+3
* Cleaned up handling of composite conditionsxleroy2011-08-051-17/+109
* Merge of branch new-semantics: revised and strengthened top-level statements ...xleroy2011-07-151-4/+3
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-131-0/+32
* Renamed Machconcr into Machsem.xleroy2011-04-091-53/+53
* Merge of branch "unsigned-offsets":xleroy2011-04-091-66/+110
* Improvements for int8 and int16 storesxleroy2010-09-101-1/+3
* Merge of the reuse-temps branch:xleroy2010-09-021-0/+1229