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
Showing
- arm/Asmgenproof1.v 2 additions, 2 deletionsarm/Asmgenproof1.v
- arm/ConstpropOp.v 9 additions, 9 deletionsarm/ConstpropOp.v
- arm/ConstpropOpproof.v 8 additions, 8 deletionsarm/ConstpropOpproof.v
- arm/Op.v 20 additions, 20 deletionsarm/Op.v
- arm/SelectOp.v 4 additions, 4 deletionsarm/SelectOp.v
- arm/SelectOpproof.v 10 additions, 10 deletionsarm/SelectOpproof.v
- backend/Cminor.v 3 additions, 3 deletionsbackend/Cminor.v
- backend/Selectionproof.v 3 additions, 3 deletionsbackend/Selectionproof.v
- cfrontend/Cminorgenproof.v 3 additions, 3 deletionscfrontend/Cminorgenproof.v
- cfrontend/Csem.v 3 additions, 3 deletionscfrontend/Csem.v
- common/Values.v 17 additions, 21 deletionscommon/Values.v
- lib/Coqlib.v 23 additions, 5 deletionslib/Coqlib.v
- lib/Integers.v 481 additions, 389 deletionslib/Integers.v
- powerpc/Asm.v 0 additions, 2 deletionspowerpc/Asm.v
- powerpc/Asmgenproof1.v 7 additions, 7 deletionspowerpc/Asmgenproof1.v
- powerpc/ConstpropOp.v 14 additions, 14 deletionspowerpc/ConstpropOp.v
- powerpc/ConstpropOpproof.v 13 additions, 13 deletionspowerpc/ConstpropOpproof.v
- powerpc/Op.v 20 additions, 20 deletionspowerpc/Op.v
- powerpc/SelectOp.v 4 additions, 4 deletionspowerpc/SelectOp.v
- powerpc/SelectOpproof.v 8 additions, 12 deletionspowerpc/SelectOpproof.v
Loading
Please register or sign in to comment