aboutsummaryrefslogtreecommitdiff
path: root/engine/dune
diff options
context:
space:
mode:
Diffstat (limited to 'engine/dune')
-rw-r--r--engine/dune6
1 files changed, 6 insertions, 0 deletions
diff --git a/engine/dune b/engine/dune
new file mode 100644
index 0000000000..e2b7ab9c87
--- /dev/null
+++ b/engine/dune
@@ -0,0 +1,6 @@
+(library
+ (name engine)
+ (synopsis "Coq's Tactic Engine")
+ (public_name coq.engine)
+ (wrapped false)
+ (libraries library))