aboutsummaryrefslogtreecommitdiffstats
path: root/backend/RREproof.v
Commit message (Expand)AuthorAgeFilesLines
* Assorted changes to reduce stack and heap requirements when compiling very bi...xleroy2013-03-161-27/+57
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.xleroy2013-01-291-4/+4
* Remove some useless "Require".xleroy2012-12-301-1/+0
* Harden proof script against empty destroyed_at_movexleroy2011-08-221-7/+6
* New backend pass "RRE": optimize (somewhat) redundant reloads introduced by t...xleroy2011-08-161-0/+630