aboutsummaryrefslogtreecommitdiffstats
path: root/backend/CminorSel.v
Commit message (Expand)AuthorAgeFilesLines
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-7/+7
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-9/+2
* Cminor, CminorSel: removed useless premises in rules for Sreturnxleroy2009-01-041-2/+0
* Fusion partielle de la branche contsem: xleroy2008-07-081-176/+189
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...xleroy2007-08-281-133/+196
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-0/+296