summaryrefslogtreecommitdiff
path: root/backend/RREproof.v
Commit message (Expand)AuthorAge
* Assorted changes to reduce stack and heap requirements when compiling very bi...Gravatar xleroy2013-03-16
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.Gravatar xleroy2013-01-29
* Remove some useless "Require".Gravatar xleroy2012-12-30
* Harden proof script against empty destroyed_at_moveGravatar xleroy2011-08-22
* New backend pass "RRE": optimize (somewhat) redundant reloads introduced by t...Gravatar xleroy2011-08-16