diff --git a/_CoqProject b/_CoqProject
index 5cc5e5b..e40d719 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -10,7 +10,6 @@ theories/Buch.v
 theories/CoefStructure.v
 theories/Dickson.v
 theories/DivTerm.v
-theories/Extract.v
 theories/Fred.v
 theories/LetP.v
 theories/LexiOrder.v
@@ -34,3 +33,4 @@ theories/Pspminus.v
 theories/Pspoly.v
 theories/Term.v
 theories/WfR0.v
+src/Extract.v
diff --git a/dune-project b/dune-project
index e49d7d3..52cdf33 100644
--- a/dune-project
+++ b/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.4)
-(using coq 0.1)
+(lang dune 2.5)
+(using coq 0.2)
 (name coq-buchberger)
diff --git a/theories/Extract.v b/src/Extract.v
similarity index 99%
rename from theories/Extract.v
rename to src/Extract.v
index 216f6fd..7d0c5f7 100644
--- a/theories/Extract.v
+++ b/src/Extract.v
@@ -9,8 +9,8 @@
 (*                                                                           *)
 (*****************************************************************************)
 
-Require Import LexiOrder.
-Require Import BuchRed.
+Require Import Buchberger.LexiOrder.
+Require Import Buchberger.BuchRed.
 Require Extraction.
 
 Extraction
diff --git a/src/dune b/src/dune
new file mode 100644
index 0000000..5ee0c76
--- /dev/null
+++ b/src/dune
@@ -0,0 +1,5 @@
+(coq.extraction
+ (prelude Extract)
+ (extracted_modules sin_num)
+ (theories Buchberger)
+ (flags -w -extraction-opaque-accessed))