aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Csyntax.v
Commit message (Expand)AuthorAgeFilesLines
* Function types didn't always degrade to pointers like they should. Introduce...xleroy2010-03-021-19/+22
* Transition semantics for Clight and Csharpminorxleroy2009-08-031-1/+8
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-26/+26
* Clight: ajout Econdition, suppression Eindex.xleroy2008-09-271-1/+91
* Utilisation de intoffloatu. Ajout du cas int + ptr.xleroy2008-05-311-0/+3
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+15
* In Clight, revised handling of comparisons between pointers and 0xleroy2007-11-131-10/+8
* Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les express...xleroy2007-08-281-7/+2
* Documentationxleroy2007-08-051-107/+192
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-4/+7
* Revu traitement des structures et unions recursives. Dans Cshmgen, meilleure...xleroy2006-09-111-8/+12
* Revu traitement des variables globales dans AST.program et dans Globalenvs.xleroy2006-09-051-16/+1
* Fusion de la branche "traces":xleroy2006-09-041-0/+456