diff options
Diffstat (limited to 'powerpc/SelectOp.vp')
-rw-r--r-- | powerpc/SelectOp.vp | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index fbd2d7b4..905a4489 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -37,14 +37,9 @@ *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Cminor. Require Import Op. Require Import CminorSel. |