summaryrefslogtreecommitdiff
path: root/ia32/ConstpropOp.vp
diff options
context:
space:
mode:
Diffstat (limited to 'ia32/ConstpropOp.vp')
-rw-r--r--ia32/ConstpropOp.vp1
1 files changed, 0 insertions, 1 deletions
diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index ff5044f..8a612f0 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/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.