summaryrefslogtreecommitdiff
path: root/backend/CMparser.mly
Commit message (Expand)AuthorAge
* Constant propagation within __builtin_annot.Gravatar xleroy2013-02-24
* Ported to Coq 8.4pl1. Merge of branches/coq-8.4.Gravatar xleroy2013-01-29
* Update Cminor parser and printer so that the parser can parse the whole Cmino...Gravatar xleroy2013-01-07
* Merge of the clightgen branch:Gravatar xleroy2012-12-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
* Use Flocq for floatsGravatar xleroy2012-06-28
* Minor updatesGravatar xleroy2012-03-11
* Merge of Andrew Tolmach's HASP-related changesGravatar xleroy2012-03-09
* 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
* Support for inlined built-ins.Gravatar xleroy2010-06-29
* Updated Caml parts to match new representation for global variables.Gravatar xleroy2010-05-26
* 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
* Fixed unary minusGravatar xleroy2009-01-07
* Reorganized the development, modularizing away machine-dependent parts.Gravatar xleroy2008-12-30