aboutsummaryrefslogtreecommitdiffstats
path: root/backend/RTLtypingaux.ml
Commit message (Expand)AuthorAgeFilesLines
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsxleroy2011-10-181-3/+3
* Revised handling of annotation statements, and more generally built-in functi...xleroy2011-06-131-2/+3
* Merge of the reuse-temps branch:xleroy2010-09-021-0/+2
* Support for inlined built-ins.xleroy2010-06-291-0/+11
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-0/+1
* Added support for jump tables in back end.xleroy2009-11-101-0/+2
* Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive f...xleroy2009-01-291-1/+0
* Elimination of "alloc" instruction in Caml files and test files.xleroy2009-01-111-2/+0
* Reorganized the development, modularizing away machine-dependent parts.xleroy2008-12-301-0/+156