diff options
Diffstat (limited to 'arm/SelectOp.vp')
-rw-r--r-- | arm/SelectOp.vp | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index 255c97c1..22ef88d2 100644 --- a/arm/SelectOp.vp +++ b/arm/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. |