aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Inliningspec.v
Commit message (Expand)AuthorAgeFilesLines
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-1/+32
* Pointers one pastxleroy2013-02-151-2/+2
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-3/+3
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Globalenvs: allocate one-byte block with permissions Nonempty for eachxleroy2012-11-121-35/+16
* Merge of the newmem branch:xleroy2012-05-211-0/+712