aboutsummaryrefslogtreecommitdiffstats
path: root/ia32/Asmgenproof.v
Commit message (Expand)AuthorAgeFilesLines
* Add Genv.public_symbol operation.Xavier Leroy2014-11-241-4/+12
* Merge of "newspilling" branch:xleroy2014-07-231-10/+5
* Refactoring: move symbol_offset into Genv.xleroy2014-05-241-4/+4
* Future-proofing: keep signature information in IA32 and PowerPC Asm, just lik...xleroy2013-12-261-17/+17
* Merge of the "princeton" branch:xleroy2013-06-161-1/+1
* Merge of the float32 branch: xleroy2013-05-191-0/+4
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-81/+50
* Assorted changes to reduce stack and heap requirements when compiling very bi...xleroy2013-03-161-4/+5
* Glasnost: making transparent a number of definitions that were opaquexleroy2013-03-101-2/+2
* Finished backtracking (cf previous commit) for ARM and PowerPC.xleroy2013-03-041-41/+4
* Partial backtracking on previous commit: the "hole in Mach stack frame" xleroy2013-03-031-280/+232
* Revised Stacking and Asmgen passes and Mach semantics: xleroy2013-03-011-653/+280
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-10/+12
* 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