diff options
Diffstat (limited to 'powerpc/CombineOp.v')
-rw-r--r-- | powerpc/CombineOp.v | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/powerpc/CombineOp.v b/powerpc/CombineOp.v index 5cb76308..6ad6987d 100644 --- a/powerpc/CombineOp.v +++ b/powerpc/CombineOp.v @@ -17,13 +17,7 @@ Require Import Coqlib. Require Import AST. Require Import Integers. Require Import Op. -Require SelectOp. - -Definition valnum := positive. - -Inductive rhs : Type := - | Op: operation -> list valnum -> rhs - | Load: memory_chunk -> addressing -> list valnum -> rhs. +Require Import CSEdomain. Section COMBINE. |