aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Integers.v
Commit message (Expand)AuthorAgeFilesLines
...
* - Added alignment constraints to memory loads and stores.xleroy2009-01-111-53/+0
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.xleroy2008-12-291-258/+638
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+15
* Preuve des 2 axiomes restantsxleroy2007-03-021-2/+17
* Petites adaptations pour Coq 8.1gammaxleroy2006-11-111-14/+22
* Fusion de la branche "traces":xleroy2006-09-041-36/+35
* Initial import of compcertxleroy2006-02-091-0/+2184