Merge pull request #12 from gares/opam2

Opam2

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)

opam

@@ -1,17 +1,24 @@
-opam-version: "1.0"
+opam-version: "2.0"
 name: "coq-mathcomp-fourcolor"
 version: "dev"
 maintainer: "Mathematical Components <[email protected]>"
-
 homepage: "https://math-comp.github.io/math-comp/"
 bug-reports: "Mathematical Components <[email protected]>"
-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.
+"""