summaryrefslogtreecommitdiff
path: root/caml/Camlcoq.ml
Commit message (Expand)AuthorAge
* Reorganized the development, modularizing away machine-dependent parts.Gravatar xleroy2008-12-30
* Extract Coq lists to Caml lists.Gravatar xleroy2008-12-29
* Camlcoq.ml: interpret Caml's int32 as unsigned when converting to Integers.intGravatar xleroy2008-04-16
* Ajout license, README, copyright noticesGravatar xleroy2008-01-27
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".Gravatar xleroy2007-08-04
* Code de timingGravatar xleroy2006-09-11
* Integration du front-end CIL developpe par Thomas MoniotGravatar xleroy2006-09-07
* Definition redondanteGravatar xleroy2006-09-06
* Fusion de la branche "traces":Gravatar xleroy2006-09-04
* Ajout d'un type-checker (non certifie) pour CminorGravatar xleroy2006-07-17
* Renommage List -> CList lors de l'extractionGravatar xleroy2006-03-09
* Initial import of compcertGravatar xleroy2006-02-09