diff --git a/Makefile b/Makefile
index 470e3507bc8bab739f971d93d349f8a2b9d5727a..611e9da846d69cd4e2687f4d630dd1ae75b25b2e 100644
--- a/Makefile
+++ b/Makefile
@@ -19,7 +19,7 @@
 ##########################################################################
 
 all:
-	dune build --root=$$(pwd) @install colibri2.opam colibrics.opam
+	dune build --root=$$(pwd) @install colibri2.opam colibrics.opam farith.opam
 
 test:
 	dune runtest --root=$$(pwd)
diff --git a/dune-project b/dune-project
index 88df0928208a5a1dd59555a696626256b9953427..11f201f5e1cca3cde351be9ee724499858e5ba3e 100644
--- a/dune-project
+++ b/dune-project
@@ -53,3 +53,12 @@
            ("ocaml" (>= "4.08"))
          )
 )
+
+(package (name farith)
+         (authors "François Bobot" "Loïc Correnson")
+         (maintainers "François Bobot")
+         (license LGPL-3.0-only)
+         (synopsis "A Library for IEEE floating points number with fixed arbitary exponent and mantissa size")
+         (description "Obtained from extraction of the Flocq library proved in Coq")
+         (depends "zarith")
+)
diff --git a/farith.opam b/farith.opam
new file mode 100644
index 0000000000000000000000000000000000000000..d7be0ffae6b8763f607458607bf52faf6dd44214
--- /dev/null
+++ b/farith.opam
@@ -0,0 +1,30 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis:
+  "A Library for IEEE floating points number with fixed arbitary exponent and mantissa size"
+description: "Obtained from extraction of the Flocq library proved in Coq"
+maintainer: ["François Bobot"]
+authors: ["François Bobot" "Loïc Correnson"]
+license: "LGPL-3.0-only"
+homepage: "https://git.frama-c.com/bobot/colibrics"
+bug-reports: "https://git.frama-c.com/bobot/colibrics/issues"
+depends: [
+  "dune" {>= "2.8"}
+  "zarith"
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://git.frama-c.com/bobot/colibrics.git"
diff --git a/farith/dune-project b/farith/dune-project
deleted file mode 100644
index de4fc20920050d2aa187123f17080218ff2ac041..0000000000000000000000000000000000000000
--- a/farith/dune-project
+++ /dev/null
@@ -1 +0,0 @@
-(lang dune 1.0)
diff --git a/farith/farith.opam b/farith/farith.opam
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000