summaryrefslogtreecommitdiff
path: root/backend/RTLtypingaux.ml
Commit message (Expand)AuthorAge
* 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 the reuse-temps branch:Gravatar xleroy2010-09-02
* Support for inlined built-ins.Gravatar xleroy2010-06-29
* Merge of the newmem and newextcalls branches:Gravatar xleroy2010-03-07
* Added support for jump tables in back end.Gravatar xleroy2009-11-10
* Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive f...Gravatar xleroy2009-01-29
* Elimination of "alloc" instruction in Caml files and test files.Gravatar xleroy2009-01-11
* Reorganized the development, modularizing away machine-dependent parts.Gravatar xleroy2008-12-30