diff --git a/.gitignore b/.gitignore
index 778fbf3..3de8881 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,6 +1,9 @@
 # Generated Makefile
-/Makefile.coq
-/Makefile.coq.conf
+Makefile.coq
+Makefile.coq.conf
+
+# Dune
+_build
 
 # Make dependencies
 *.d
diff --git a/Makefile b/Makefile
index d4d7fad..ad909e5 100644
--- a/Makefile
+++ b/Makefile
@@ -1,14 +1,16 @@
-# -*- Makefile -*-
-.PHONY: coq clean
+all: Makefile.coq
+	@+$(MAKE) -f Makefile.coq all
 
-coq:: Makefile.coq
-	$(MAKE) -f Makefile.coq
+clean: Makefile.coq
+	@+$(MAKE) -f Makefile.coq cleanall
+	@rm -f Makefile.coq Makefile.coq.conf
 
-Makefile.coq: Make.cfg
-	coq_makefile -f Make.cfg -o Makefile.coq
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-distclean:
-	rm -f Makefile.coq Makefile.coq.conf Makefile.coq.bak .coqdeps.d
+force _CoqProject Makefile: ;
 
-install:
-	$(MAKE) -f Makefile.coq install
+%: Makefile.coq force
+	@+$(MAKE) -f Makefile.coq $@
+
+.PHONY: all clean force
diff --git a/Make.cfg b/_CoqProject
similarity index 79%
rename from Make.cfg
rename to _CoqProject
index 7984b76..d8dfbb2 100644
--- a/Make.cfg
+++ b/_CoqProject
@@ -1,3 +1,4 @@
+-R theories Param
 -R src Param
 -I src
 src/debug.ml
@@ -6,3 +7,4 @@ src/relations.ml
 src/declare_translation.ml
 src/abstraction.mlg
 src/paramcoq.mlpack
+theories/Param.v
diff --git a/dune-project b/dune-project
new file mode 100644
index 0000000..6111640
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,3 @@
+(lang dune 2.5)
+(using coq 0.2)
+(name paramcoq)
diff --git a/src/dune b/src/dune
index 177bd59..3c06cd2 100644
--- a/src/dune
+++ b/src/dune
@@ -1,11 +1,8 @@
 (library
  (name paramcoq)
- (public_name coq.plugins.paramcoq)
- (synopsis "Coq Plugin for Parametricity")
- (flags :standard -warn-error -3)
- (libraries coq.plugins.ltac))
+ (public_name coq-paramcoq.plugin)
+ (synopsis "Plugin for generating parametricity statements to perform refinement proofs")
+ (flags :standard -rectypes -w -9-27)
+ (libraries coq-core.plugins.ltac))
 
-(rule
- (targets abstraction.ml)
- (deps (:pp-file abstraction.mlg) )
- (action (run coqpp %{pp-file})))
+(coq.pp (modules abstraction))
diff --git a/theories/Param.v b/theories/Param.v
new file mode 100644
index 0000000..c3a74b5
--- /dev/null
+++ b/theories/Param.v
@@ -0,0 +1 @@
+Declare ML Module "paramcoq".
diff --git a/theories/dune b/theories/dune
new file mode 100644
index 0000000..d65823a
--- /dev/null
+++ b/theories/dune
@@ -0,0 +1,5 @@
+(coq.theory
+ (name Param)
+ (package coq-paramcoq)
+ (synopsis "Plugin for generating parametricity statements to perform refinement proofs")
+ (libraries coq-paramcoq.plugin))