summaryrefslogtreecommitdiff
path: root/arm/ValueAOp.v
diff options
context:
space:
mode:
Diffstat (limited to 'arm/ValueAOp.v')
-rw-r--r--arm/ValueAOp.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/arm/ValueAOp.v b/arm/ValueAOp.v
index c968213..037b22e 100644
--- a/arm/ValueAOp.v
+++ b/arm/ValueAOp.v
@@ -11,6 +11,7 @@
(* *********************************************************************)
Require Import Coqlib.
+Require Import Compopts.
Require Import AST.
Require Import Integers.
Require Import Floats.