aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/SelectOp.vp
diff options
context:
space:
mode:
Diffstat (limited to 'riscV/SelectOp.vp')
-rw-r--r--riscV/SelectOp.vp12
1 files changed, 7 insertions, 5 deletions
diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index ba7c5664..e9920e46 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -44,11 +44,8 @@
Require Archi.
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.
@@ -461,3 +458,8 @@ Definition divf_base (e1: expr) (e2: expr) :=
Definition divfs_base (e1: expr) (e2: expr) :=
Eop Odivfs (e1 ::: e2 ::: Enil).
+
+(** Platform-specific known builtins *)
+
+Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
+ None.