aboutsummaryrefslogtreecommitdiffstats
path: root/ia32/SelectOp.vp
diff options
context:
space:
mode:
Diffstat (limited to 'ia32/SelectOp.vp')
-rw-r--r--ia32/SelectOp.vp2
1 files changed, 0 insertions, 2 deletions
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index bd3a4850..744902ec 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -521,5 +521,3 @@ Nondetfunction builtin_arg (e: expr) :=
| Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs
| _ => BA e
end.
-
-Definition builtin_function_const (id: ident) := false.