aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun/dune
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/byterun/dune')
-rw-r--r--kernel/byterun/dune6
1 files changed, 5 insertions, 1 deletions
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index d3e2a2fa7f..b14ad5c558 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -1,7 +1,7 @@
(library
(name byterun)
(synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
- (public_name coq.vm)
+ (public_name coq-core.vm)
(foreign_stubs
(language c)
(names coq_fix_code coq_float64 coq_memory coq_values coq_interp)
@@ -14,3 +14,7 @@
(rule
(targets coq_jumptbl.h)
(action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe jump))))
+
+(rule
+ (targets coq_arity.h)
+ (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe arity))))