diff options
Diffstat (limited to 'kernel/dune')
| -rw-r--r-- | kernel/dune | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/kernel/dune b/kernel/dune new file mode 100644 index 0000000000..a503238907 --- /dev/null +++ b/kernel/dune @@ -0,0 +1,20 @@ +(library + (name kernel) + (synopsis "The Coq Kernel") + (public_name coq.kernel) + (wrapped false) + (modules_without_implementation cinstr nativeinstr) + (libraries clib config lib byterun)) + +(rule + (targets copcodes.ml) + (deps (:h-file byterun/coq_instruct.h) make-opcodes) + (action (run ./make_opcodes.sh %{h-file} %{targets}))) + +(documentation + (package coq)) + +; In dev profile, we check the kernel against a more strict set of +; warnings. +(env + (dev (flags :standard -w +a-4-44-50))) |