summaryrefslogtreecommitdiff
path: root/Changelog
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-11-19 13:32:09 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-11-19 13:32:09 +0000
commitef40c6d36f1c3125f3aa78ea4eaa61dcc7bcae67 (patch)
tree7bd176bb0dbf60617954fabadd8aedc64b4cf647 /Changelog
parentcdf83055d96e2af784a97c783c94b83ba2032ae1 (diff)
Revised lib/Integers.v to make it parametric w.r.t. word size.
Introduced Int.iwordsize and used it in place of "Int.repr 32" or "Int.repr (Z_of_nat wordsize)". git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'Changelog')
0 files changed, 0 insertions, 0 deletions