aboutsummaryrefslogtreecommitdiffstats
path: root/extraction/extraction.v
Commit message (Expand)AuthorAgeFilesLines
* Flag to turn on/off the recognition of fused multiply-add and multiply-subxleroy2008-07-311-0/+3
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...xleroy2008-05-301-0/+1
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+12
* Simplification des Cconst_symbol: seules les versions 'signed' sont conserveesxleroy2007-10-311-4/+2
* Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFGxleroy2007-10-271-0/+3
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-0/+1
* Fusion de la branche "traces":xleroy2006-09-041-4/+14
* Initial import of compcertxleroy2006-02-091-0/+53