summaryrefslogtreecommitdiff
path: root/backend/Inliningspec.v
Commit message (Expand)AuthorAge
* Inlining: preserve all RTL regs mentioned in the function, not justGravatar xleroy2014-03-29
* Revised renumbering of nodes and registers so that main function is not shift...Gravatar xleroy2013-10-18
* Merge of the "princeton" branch:Gravatar xleroy2013-06-16
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:Gravatar xleroy2013-04-20
* Pointers one pastGravatar xleroy2013-02-15
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.Gravatar xleroy2013-01-29
* Remove some useless "Require".Gravatar xleroy2012-12-30
* Globalenvs: allocate one-byte block with permissions Nonempty for eachGravatar xleroy2012-11-12
* Merge of the newmem branch:Gravatar xleroy2012-05-21