summaryrefslogtreecommitdiff
path: root/backend/PrintMach.ml
Commit message (Expand)AuthorAge
* Do not use Format for faster printing of RTL, XTL, LTL, MachGravatar xleroy2013-09-26
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:Gravatar xleroy2013-04-20
* 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
* Revised handling of annotation statements, and more generally built-in functi...Gravatar xleroy2011-06-13
* powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).Gravatar xleroy2011-05-08