aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Compiler.v
Commit message (Expand)AuthorAgeFilesLines
* powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).xleroy2011-05-081-3/+4
* Added pass CleanupLabels to remove unreferenced labels in a proved way.xleroy2011-05-081-3/+11
* Renamed Machconcr into Machsem.xleroy2011-04-091-0/+1
* Merge of branch "unsigned-offsets":xleroy2011-04-091-2/+0
* More global initialization work done and proved in Coq.xleroy2011-03-131-1/+1
* Initializers for global variables: compile-time evaluation of expressions don...xleroy2011-03-121-0/+5
* Merge of branches/full-expr-4:xleroy2010-08-181-65/+103
* Support for inlined built-ins.xleroy2010-06-291-11/+11
* Merging the Princeton implementation of the memory model. Separate axioms in...xleroy2010-06-281-0/+1
* Added 'going wrong' behaviorsxleroy2009-08-051-30/+32
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-7/+7
* Added tail call optimization passxleroy2009-03-261-2/+9
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-0/+305