1 files changed, 7 insertions, 5 deletions
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index d04832d6..1220abc4 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -38,11 +38,8 @@
 
 Require Import Coqlib.
 Require Import Compopts.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Op.
-Require Import CminorSel.
+Require Import AST Integers Floats Builtins.
+Require Import Op CminorSel.
 
 Local Open Scope cminorsel_scope.
 
@@ -518,3 +515,8 @@ Nondetfunction builtin_arg (e: expr) :=
   | Eop (Oaddimm n) (e1:::Enil) => BA_addptr (BA e1) (BA_int n)
   | _ => BA e
   end.
+
+(** Platform-specific known builtins *)
+
+Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
+  None.