diff --git a/README.md b/README.md
index 9d20f7fb93fce30d52e3dc590f9d3c4ceb9b24f8..95a35234757169aecf5bb024dbd048c6bc72289b 100644
--- a/README.md
+++ b/README.md
@@ -8,7 +8,7 @@ COLIBRICS written in Eclipse Prolog by Bruno Marre
 Using [opam](http://opam.ocaml.org/):
 
 ```shell
-opam pin add colibri2  https://git.frama-c.com/bobot/colibri2.git
+opam pin add https://git.frama-c.com/bobot/colibri2.git
 ```
 
 ## Development ##
diff --git a/colibrics.opam b/colibrics.opam
index 09cd7ff218dd8e7b2379f89698d1cc6445ea20d4..8df0d602da066409702e8d3982ca0fb32f4c4465 100644
--- a/colibrics.opam
+++ b/colibrics.opam
@@ -1,5 +1,10 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
+synopsis: "A CP solver proved in Why3"
+description:
+  "The core of Colibrics is formally proved using Why3. It offers also libraries that define formally proved simple propagation domains "
+maintainer: ["François Bobot"]
+authors: ["François Bobot"]
 homepage: "https://git.frama-c.com/bobot/colibrics"
 bug-reports: "https://git.frama-c.com/bobot/colibrics/issues"
 depends: [
diff --git a/dune-project b/dune-project
index 65842d36c727c0e59ebe26026226f9990b0e4b0d..d012b637e7accd50af3a802d1c5a11a5ec1d4049 100644
--- a/dune-project
+++ b/dune-project
@@ -6,6 +6,10 @@
 (name colibrics)
 (package
   (name colibrics)
+  (authors "François Bobot")
+  (maintainers "François Bobot")
+  (synopsis "A CP solver proved in Why3")
+  (description "The core of Colibrics is formally proved using Why3. It offers also libraries that define formally proved simple propagation domains ")
   (depends
     "ppx_deriving_yojson"
     ("dolmen" (>= "0.5~dev"))