| Commit message (Expand) | Author | Age | Files | Lines |
* | Reorganized the development, modularizing away machine-dependent parts. | xleroy | 2008-12-30 | 4 | -646/+26 |
* | Extract Coq lists to Caml lists. | xleroy | 2008-12-29 | 2 | -2/+4 |
* | Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext. | xleroy | 2008-12-29 | 1 | -3/+9 |
* | Revised back-end so that only 2 integer registers are reserved for reloading. | xleroy | 2008-12-21 | 1 | -4/+0 |
* | Flag to turn on/off the recognition of fused multiply-add and multiply-sub | xleroy | 2008-07-31 | 3 | -27/+33 |
* | Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ... | xleroy | 2008-05-30 | 2 | -5/+9 |
* | Compilo C, preprocesseur, assembleur sont determines par configure et mis dan... | xleroy | 2008-04-19 | 1 | -1/+5 |
* | MAJ | xleroy | 2008-04-15 | 1 | -123/+121 |
* | Ajout license, README, copyright notices | xleroy | 2008-01-27 | 2 | -0/+24 |
* | Problemes d'alignement des variables globales et a l'interieur de leurs initi... | xleroy | 2007-10-31 | 1 | -112/+116 |
* | Simplification des Cconst_symbol: seules les versions 'signed' sont conservees | xleroy | 2007-10-31 | 1 | -4/+2 |
* | Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFG | xleroy | 2007-10-27 | 4 | -35/+19 |
* | MAJ | xleroy | 2007-10-17 | 1 | -107/+107 |
* | Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express... | xleroy | 2007-08-28 | 2 | -127/+121 |
* | Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefiles | xleroy | 2007-08-06 | 2 | -114/+138 |
* | Fusion des modifications faites sur les branches "tailcalls" et "smallstep". | xleroy | 2007-08-04 | 4 | -165/+233 |
* | Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de... | xleroy | 2007-03-02 | 3 | -137/+145 |
* | Lever la restriction sur les fonctions externes, restriction qui exigeait que... | xleroy | 2006-10-22 | 1 | -10/+15 |
* | MAJ suite ajouts dans Kildall. Compiler en code natif par defaut | xleroy | 2006-09-11 | 2 | -11/+29 |
* | Encore une eta-expansion intempestive | xleroy | 2006-09-11 | 1 | -4/+23 |
* | MAJ | xleroy | 2006-09-08 | 1 | -2/+2 |
* | Integration du front-end CIL developpe par Thomas Moniot | xleroy | 2006-09-07 | 2 | -29/+45 |
* | Ajout de dependances dans extraction/Makefile | tristan | 2006-09-06 | 2 | -23/+31 |
* | Revu la repartition des sources Coq en sous-repertoires | xleroy | 2006-09-04 | 1 | -1/+1 |
* | Fusion de la branche "traces": | xleroy | 2006-09-04 | 3 | -101/+124 |
* | Ajout d'un type-checker (non certifie) pour Cminor | xleroy | 2006-07-17 | 2 | -15/+20 |
* | Renommage List -> CList lors de l'extraction | xleroy | 2006-03-09 | 2 | -219/+221 |
* | Nettoyages | xleroy | 2006-02-09 | 1 | -1/+4 |
* | Initial import of compcert | xleroy | 2006-02-09 | 6 | -0/+589 |