fix coq-mathcomp-bigenough

packages/coq-mathcomp-bigenough/coq-mathcomp-bigenough.1.0.0/opam

-opam-version: "1.2"
+opam-version: "2.0"
 name: "coq-mathcomp-bigenough"
-version: "dev"
+version: "1.0.0"
 maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
 
 homepage: "https://github.com/math-comp/bigenough"
 bug-reports: "https://github.com/math-comp/bigenough/issues"
 license: "CeCILL-B"
+dev-repo: "git+https://github.com/math-comp/bigenough"
 
 build: [ make "-j" "%{jobs}%" ]
 install: [ make "install" ]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/bigenough'" ]
-depends: [ "coq-mathcomp-ssreflect" { (>= "1.6.0" | = "dev") } ]
-url {
-  src: "packages/coq-mathcomp"
-}
+depends: [
+  "ocaml"
+  "coq-mathcomp-ssreflect" {(>= "1.6" | = "dev")}
+]
 tags: [ "keyword:bigenough" "keyword:asymptotic reasonning" "keyword:small scale reflection" "keyword:mathematical components" ]
 authors: [ "Cyril Cohen <cyril.cohen@inria.fr>" ]
+synopsis: "A small library to do epsilon - N reasonning"
+description: """
+The package contains a package to reasoning with big enough objects
+(mostly natural numbers). This package is essentially for backward
+compatibility purposes as `bigenough` will be subsumed by the near
+tactics. The formalization is based on the Mathematical Components
+library."""
+url {
+  src: "packages/coq-mathcomp-bigenough/coq-mathcomp-bigenough.1.0.0"
+}
\ No newline at end of file