summaryrefslogtreecommitdiff
path: root/backend/Inliningproof.v
Commit message (Expand)AuthorAge
* Merge of "newspilling" branch:Gravatar xleroy2014-07-23
* 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
* Pointers one pastGravatar xleroy2013-02-15
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.Gravatar xleroy2013-01-29
* Globalenvs: allocate one-byte block with permissions Nonempty for eachGravatar xleroy2012-11-12
* - Revised non-overflow constraints on memory injections so that Gravatar xleroy2012-07-23
* CSE: add recognition of some combined operators, conditions, and addressing m...Gravatar xleroy2012-05-26
* Merge of the newmem branch:Gravatar xleroy2012-05-21