diff --git a/README.md b/README.md
index 0525706..3810576 100644
--- a/README.md
+++ b/README.md
@@ -2,7 +2,7 @@
 
 # The Four Color Theorem
 The repository contains a [mechanization](http://www.ams.org/notices/200811/tx081101382p.pdf) of 
-the [Four ColorTheorem](https://en.wikipedia.org/wiki/Four_color_theorem)(Appel & Haken, 1976), 
+the [Four Color Theorem](https://en.wikipedia.org/wiki/Four_color_theorem)(Appel & Haken, 1976), 
 a landmark result of graph theory.
 
 The formal proof is based on the [Mathematical Components](https://github.com/math-comp/math-comp)
diff --git a/descr b/descr
deleted file mode 100644
index fdbaf22..0000000
--- a/descr
+++ /dev/null
@@ -1,6 +0,0 @@
-Proof of the Four Color Theorem
-
-This library contains a formalized proof of the Four Color Theorem, along
-with the theories needed to support stating and then proving the Theorem.
-  This includes an axiomatization of the setoid of classical real numbers,
-basic plane topology definitions, and a theory of combinatorial hypermaps.
\ No newline at end of file
diff --git a/opam b/opam
index c00ba83..30a7ce5 100644
--- a/opam
+++ b/opam
@@ -1,17 +1,24 @@
-opam-version: "1.0"
+opam-version: "2.0"
 name: "coq-mathcomp-fourcolor"
 version: "dev"
 maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
-
 homepage: "https://math-comp.github.io/math-comp/"
 bug-reports: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
-dev-repo: "https://github.com/math-comp/fourcolor.git"
+dev-repo: "git+https://github.com/math-comp/fourcolor"
 license: "CeCILL-B"
 
 build: [ make "-j" "%{jobs}%" ]
 install: [ make "install" ]
-remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/fourcolor'" ]
 depends: [ "coq-mathcomp-algebra" { = "dev" } ]
 
 tags: [ "keyword:Four color theorem" "keyword:small scale reflection" "keyword:mathematical components" ]
 authors: [ "Georges Gonthier" ]
+synopsis: "Mechanization of the Four Color Theorem"
+description: """
+Proof of the Four Color Theorem
+
+This library contains a formalized proof of the Four Color Theorem, along
+with the theories needed to support stating and then proving the Theorem.
+  This includes an axiomatization of the setoid of classical real numbers,
+basic plane topology definitions, and a theory of combinatorial hypermaps.
+"""