summaryrefslogtreecommitdiff
path: root/backend/CMtypecheck.ml
Commit message (Expand)AuthorAge
* Treat casts int64 -> float32 as primitive operations instead of twoGravatar xleroy2013-07-03
* Merge of the float32 branch: Gravatar xleroy2013-05-19
* 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 branch seq-and-or. See Changelog for details.Gravatar xleroy2012-10-06
* - Revised non-overflow constraints on memory injections so that Gravatar xleroy2012-07-23
* Use Flocq for floatsGravatar xleroy2012-06-28
* Merge of the "volatile" branch:Gravatar xleroy2012-02-04
* Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml charsGravatar xleroy2011-10-18
* 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