aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/dune6
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index 8d8374a603..2998178be2 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -2,8 +2,10 @@
(name byterun)
(synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
(public_name coq.vm)
- (c_flags (:include %{project_root}/config/dune.c_flags))
- (c_names coq_fix_code coq_memory coq_values coq_interp))
+ (foreign_stubs
+ (language c)
+ (names coq_fix_code coq_memory coq_values coq_interp)
+ (flags (:include %{project_root}/config/dune.c_flags))))
(rule
(targets coq_instruct.h)