aboutsummaryrefslogtreecommitdiff
path: root/kernel/dune
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/dune')
-rw-r--r--kernel/dune15
1 files changed, 15 insertions, 0 deletions
diff --git a/kernel/dune b/kernel/dune
new file mode 100644
index 0000000000..011af9c28c
--- /dev/null
+++ b/kernel/dune
@@ -0,0 +1,15 @@
+(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))