Refactored Selection.v and Selectionproof.v into a machine-dependent part + a...
Refactored Selection.v and Selectionproof.v into a machine-dependent part + a machine-independent part. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Showing
- .depend 5 additions, 3 deletions.depend
- Makefile 1 addition, 1 deletionMakefile
- arm/SelectOp.v 30 additions, 229 deletionsarm/SelectOp.v
- arm/SelectOpproof.v 64 additions, 537 deletionsarm/SelectOpproof.v
- backend/CminorSel.v 122 additions, 0 deletionsbackend/CminorSel.v
- powerpc/PrintAsm.ml 2 additions, 2 deletionspowerpc/PrintAsm.ml
- powerpc/SelectOp.v 31 additions, 230 deletionspowerpc/SelectOp.v
- powerpc/SelectOpproof.v 70 additions, 546 deletionspowerpc/SelectOpproof.v
Loading
Please register or sign in to comment