aboutsummaryrefslogtreecommitdiffstats
path: root/extraction/extraction.v
Commit message (Expand)AuthorAgeFilesLines
* 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