diff options
Diffstat (limited to 'kernel/byterun/dune')
| -rw-r--r-- | kernel/byterun/dune | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/kernel/byterun/dune b/kernel/byterun/dune new file mode 100644 index 0000000000..20bdf28e54 --- /dev/null +++ b/kernel/byterun/dune @@ -0,0 +1,13 @@ +(library + (name byterun) + (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]") + (public_name coq.vm) + (c_names coq_fix_code coq_memory coq_values coq_interp)) + +(rule + (targets coq_instruct.h) + (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe enum)))) + +(rule + (targets coq_jumptbl.h) + (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe jump)))) |