aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Selectionproof.v
Commit message (Expand)AuthorAgeFilesLines
...
* Flag to turn on/off the recognition of fused multiply-add and multiply-subxleroy2008-07-311-6/+9
* Fusion partielle de la branche contsem: xleroy2008-07-081-129/+136
* Revu les comparaisons de pointeurs: == et <> sont definis entre 2 pointeurs v...xleroy2008-05-301-15/+32
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...xleroy2008-05-301-0/+1
* Meilleure selection pour if ((a && b) != 0), etcxleroy2008-03-271-20/+191
* 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-581/+524
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-0/+1240