aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/ExpansionOracle.ml
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-07-20 15:21:29 +0200
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-07-20 15:21:29 +0200
commita3319eb05543930844dedd9ac31ed1beaac3047e (patch)
treea9745571f4ed7841f4c231505df9102f3e84ee65 /aarch64/ExpansionOracle.ml
parentc3ce32da7d431069ef355296bef66b112a302b78 (diff)
downloadcompcert-kvx-a3319eb05543930844dedd9ac31ed1beaac3047e.tar.gz
compcert-kvx-a3319eb05543930844dedd9ac31ed1beaac3047e.zip
Fix compile on ARM/x86 backends
Diffstat (limited to 'aarch64/ExpansionOracle.ml')
-rw-r--r--aarch64/ExpansionOracle.ml4
1 files changed, 1 insertions, 3 deletions
diff --git a/aarch64/ExpansionOracle.ml b/aarch64/ExpansionOracle.ml
index 3b63b80d..0869007c 100644
--- a/aarch64/ExpansionOracle.ml
+++ b/aarch64/ExpansionOracle.ml
@@ -10,8 +10,6 @@
(* *)
(* *************************************************************)
-open RTLpathCommon
-
-let expanse (sb : superblock) code pm = (code, pm)
+let expanse n ibf btl = btl
let find_last_node_reg c = ()