aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/SimplLocalsproof.v
Commit message (Expand)AuthorAgeFilesLines
* driver: removed option -flonglongxleroy2013-04-221-0/+4
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-196/+48
* Pointers one pastxleroy2013-02-151-18/+27
* lib/Integers.v: revised and extended, faster implementation based onxleroy2013-02-101-3/+3
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-26/+26
* Avoid generating some obviously useless casts.xleroy2013-01-081-1/+22
* Merge of the clightgen branch:xleroy2012-12-291-0/+2277