aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/CBuiltins.ml
diff options
context:
space:
mode:
Diffstat (limited to 'riscV/CBuiltins.ml')
-rw-r--r--riscV/CBuiltins.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/riscV/CBuiltins.ml b/riscV/CBuiltins.ml
index 0c981d11..edaf586d 100644
--- a/riscV/CBuiltins.ml
+++ b/riscV/CBuiltins.ml
@@ -18,10 +18,10 @@
open C
let builtins = {
- Builtins.typedefs = [
+ builtin_typedefs = [
"__builtin_va_list", TPtr(TVoid [], [])
];
- Builtins.functions = [
+ builtin_functions = [
(* Synchronization *)
"__builtin_fence",
(TVoid [], [], false);