aboutsummaryrefslogtreecommitdiffstats
path: root/common/Values.v
Commit message (Expand)AuthorAgeFilesLines
...
* Merge of the "volatile" branch:xleroy2012-02-041-0/+7
* Merge of the nonstrict-ops branch:xleroy2012-01-141-221/+284
* Back from Oregon commit. xleroy2011-07-051-0/+6
* Float.intoffloat and Float.intuoffloat are now partial functions.xleroy2010-10-281-2/+2
* Merge of the reuse-temps branch:xleroy2010-09-021-0/+6
* More faithful semantics for volatile reads and writes.xleroy2010-05-231-0/+8
* Merge of the newmem and newextcalls branches:xleroy2010-03-071-0/+81
* Revised lib/Integers.v to make it parametric w.r.t. word size.xleroy2009-11-191-21/+17
* Adapted to work with Coq 8.2-1v1.4.1xleroy2009-06-051-2/+2
* Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >...xleroy2009-02-261-0/+17
* Replace cast{8,16}{signed,unsigned} with zero_ext and sign_ext.xleroy2008-12-291-40/+40
* Introduction de l'operation intuoffloat (float -> unsigned int). Pas encore ...xleroy2008-05-301-0/+6
* Ajout license, README, copyright noticesxleroy2008-01-271-0/+15
* Fusion des modifications faites sur les branches "tailcalls" et "smallstep".xleroy2007-08-041-0/+64
* Revu la repartition des sources Coq en sous-repertoiresxleroy2006-09-041-0/+888