aboutsummaryrefslogtreecommitdiffstats
path: root/common/Mem.v
Commit message (Expand)AuthorAgeFilesLines
* Added tail call optimization passxleroy2009-03-261-0/+20
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-61/+173
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.xleroy2008-12-291-10/+10
* Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs v...xleroy2008-05-301-0/+24
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...xleroy2008-05-301-0/+346
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+16
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-1651/+1630
* Ajout de Init_pointer (experimental)xleroy2006-09-171-1/+6
* Revu la repartition des sources Coq en sous-repertoiresxleroy2006-09-041-0/+2385