summaryrefslogtreecommitdiff
path: root/backend/PrintRTL.ml
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
* Globalenvs: allocate one-byte block with permissions Nonempty for eachGravatar xleroy2012-11-12
* Merge of the newmem branch:Gravatar xleroy2012-05-21
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsGravatar xleroy2011-10-18
* Revised handling of annotation statements, and more generally built-in functi...Gravatar xleroy2011-06-13
* Merge of branches/full-expr-4:Gravatar xleroy2010-08-18
* Pretty-printers for RTL and LTL. Not yet well integrated.Gravatar xleroy2010-05-02