summaryrefslogtreecommitdiff
path: root/arm/ConstpropOp.vp
diff options
context:
space:
mode:
Diffstat (limited to 'arm/ConstpropOp.vp')
-rw-r--r--arm/ConstpropOp.vp1
1 files changed, 0 insertions, 1 deletions
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index 0f06703..a9cbad5 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -17,7 +17,6 @@ Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Floats.
-Require Import Values.
Require Import Op.
Require Import Registers.