summaryrefslogtreecommitdiff
path: root/powerpc/ConstpropOp.vp
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc/ConstpropOp.vp')
-rw-r--r--powerpc/ConstpropOp.vp1
1 files changed, 1 insertions, 0 deletions
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index 9dbaa78..6aa0925 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -14,6 +14,7 @@
This is the machine-dependent part of [Constprop]. *)
Require Import Coqlib.
+Require Import Compopts.
Require Import AST.
Require Import Integers.
Require Import Floats.