summaryrefslogtreecommitdiff
path: root/coq
Commit message (Expand)AuthorAge
* Use "-as" to put CompCert modules in a compcert.xxx namespace.Gravatar xleroy2013-05-01
* Use Flocq for floatsGravatar xleroy2012-06-28
* Merge of the nonstrict-ops branch:Gravatar xleroy2012-01-14
* Merge of the newmem and newextcalls branches:Gravatar xleroy2010-03-07
* Reorganized the development, modularizing away machine-dependent parts.Gravatar xleroy2008-12-30
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".Gravatar xleroy2007-08-04
* Convenience commandGravatar xleroy2006-09-04