aboutsummaryrefslogtreecommitdiffstats
path: root/src/extraction/dune
diff options
context:
space:
mode:
Diffstat (limited to 'src/extraction/dune')
-rw-r--r--src/extraction/dune4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/extraction/dune b/src/extraction/dune
new file mode 100644
index 0000000..731701a
--- /dev/null
+++ b/src/extraction/dune
@@ -0,0 +1,4 @@
+(library
+ (name Extraction)
+ (public_name coqup.extraction)
+ (flags (:standard -warn-error -A)))