diff --git a/extra-dev/packages/coq-additions/coq-additions.dev/opam b/extra-dev/packages/coq-additions/coq-additions.dev/opam
index f75369a085..aa816ad2c6 100644
--- a/extra-dev/packages/coq-additions/coq-additions.dev/opam
+++ b/extra-dev/packages/coq-additions/coq-additions.dev/opam
@@ -5,8 +5,8 @@ license: "LGPL 2"
 build: [
   ["coq_makefile" "-f" "Make" "-o" "Makefile"]
   [make "-j%{jobs}%"]
-  [make "install"]
 ]
+install: [make "install"]
 remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Additions"]
 depends: [
   "ocaml"
diff --git a/extra-dev/packages/coq-bdds/coq-bdds.dev/opam b/extra-dev/packages/coq-bdds/coq-bdds.dev/opam
index 0157815553..323566cde9 100644
--- a/extra-dev/packages/coq-bdds/coq-bdds.dev/opam
+++ b/extra-dev/packages/coq-bdds/coq-bdds.dev/opam
@@ -6,8 +6,8 @@ build: [
   ["coq_makefile" "-f" "Make" "-o" "Makefile"]
   # [make "-j%{jobs}%"]
   [make]
-  [make "install"]
 ]
+install: [make "install"]
 remove: ["rm" "-R" "%{lib}%/coq/user-contrib/BDDs"]
 depends: [
   "ocaml"
diff --git a/extra-dev/packages/coq-dictionaries/coq-dictionaries.dev/opam b/extra-dev/packages/coq-dictionaries/coq-dictionaries.dev/opam
index d0c9dda0ed..f11771c6d2 100644
--- a/extra-dev/packages/coq-dictionaries/coq-dictionaries.dev/opam
+++ b/extra-dev/packages/coq-dictionaries/coq-dictionaries.dev/opam
@@ -5,8 +5,8 @@ license: "LGPL 2"
 build: [
   ["coq_makefile" "-f" "Make" "-o" "Makefile"]
   [make "-j%{jobs}%"]
-  [make "install"]
 ]
+install: [make "install"]
 remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Dictionaries"]
 depends: [
   "ocaml"
diff --git a/extra-dev/packages/coq-euler-formula/coq-euler-formula.dev/opam b/extra-dev/packages/coq-euler-formula/coq-euler-formula.dev/opam
index 60efa512ce..0bd3fbded4 100644
--- a/extra-dev/packages/coq-euler-formula/coq-euler-formula.dev/opam
+++ b/extra-dev/packages/coq-euler-formula/coq-euler-formula.dev/opam
@@ -5,8 +5,8 @@ license: "LGPL"
 build: [
   ["coq_makefile" "-f" "Make" "-o" "Makefile"]
   [make "-j%{jobs}%"]
-  [make "install"]
 ]
+install: [make "install"]
 remove: ["rm" "-R" "%{lib}%/coq/user-contrib/EulerFormula"]
 depends: [
   "ocaml"
diff --git a/extra-dev/packages/coq-float/coq-float.dev/opam b/extra-dev/packages/coq-float/coq-float.dev/opam
index 9f7d95f80f..48d7b82e5e 100644
--- a/extra-dev/packages/coq-float/coq-float.dev/opam
+++ b/extra-dev/packages/coq-float/coq-float.dev/opam
@@ -5,8 +5,8 @@ license: "LGPL 2"
 build: [
   ["coq_makefile" "-f" "Make" "-o" "Makefile"]
   [make "-j%{jobs}%"]
-  [make "install"]
 ]
+install: [make "install"]
 remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Float"]
 depends: [
   "ocaml"
diff --git a/extra-dev/packages/coq-hardware/coq-hardware.dev/opam b/extra-dev/packages/coq-hardware/coq-hardware.dev/opam
index d89b4a9d88..3bff7b9c0e 100644
--- a/extra-dev/packages/coq-hardware/coq-hardware.dev/opam
+++ b/extra-dev/packages/coq-hardware/coq-hardware.dev/opam
@@ -5,8 +5,8 @@ license: "LGPL 2"
 build: [
   ["coq_makefile" "-f" "Make" "-o" "Makefile"]
   [make "-j%{jobs}%"]
-  [make "install"]
 ]
+install: [make "install"]
 remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Hardware"]
 depends: [
   "ocaml"
diff --git a/extra-dev/packages/coq-ieee754/coq-ieee754.dev/opam b/extra-dev/packages/coq-ieee754/coq-ieee754.dev/opam
index 74bf28a7b5..7cdb0ddaf0 100644
--- a/extra-dev/packages/coq-ieee754/coq-ieee754.dev/opam
+++ b/extra-dev/packages/coq-ieee754/coq-ieee754.dev/opam
@@ -5,8 +5,8 @@ license: "LGPL 2"
 build: [
   ["coq_makefile" "-f" "Make" "-o" "Makefile"]
   [make "-j%{jobs}%"]
-  [make "install"]
 ]
+install: [make "install"]
 remove: ["rm" "-R" "%{lib}%/coq/user-contrib/IEEE754"]
 depends: [
   "ocaml"
diff --git a/extra-dev/packages/coq-int-map/coq-int-map.dev/opam b/extra-dev/packages/coq-int-map/coq-int-map.dev/opam
index 7713fe7b19..40f2ad04df 100644
--- a/extra-dev/packages/coq-int-map/coq-int-map.dev/opam
+++ b/extra-dev/packages/coq-int-map/coq-int-map.dev/opam
@@ -5,8 +5,8 @@ license: "LGPL 2"
 build: [
   ["coq_makefile" "-f" "Make" "-o" "Makefile"]
   [make "-j%{jobs}%"]
-  [make "install"]
 ]
+install: [make "install"]
 remove: ["rm" "-R" "%{lib}%/coq/user-contrib/IntMap"]
 depends: [
   "ocaml"
diff --git a/extra-dev/packages/coq-mathcomp-grobner/coq-mathcomp-grobner.dev/opam b/extra-dev/packages/coq-mathcomp-grobner/coq-mathcomp-grobner.dev/opam
index 63c158fa3a..f4a5cb1088 100644
--- a/extra-dev/packages/coq-mathcomp-grobner/coq-mathcomp-grobner.dev/opam
+++ b/extra-dev/packages/coq-mathcomp-grobner/coq-mathcomp-grobner.dev/opam
@@ -1,25 +1,26 @@
 opam-version: "2.0"
 maintainer: "Laurent.Thery@inria.fr"
 homepage: "https://github.com/thery/grobner"
+dev-repo: "git+https://github.com/thery/grobner.git"
 bug-reports: "https://github.com/thery/grobner/issues"
 license: "MIT"
-build: [
-  ["./configure.sh"]
-  [make "-j%{jobs}%"]
-  [make "install"]
+authors: [
+  "Laurent Théry"
 ]
+build: [make "-j%{jobs}%"]
+install: [make "install"]
 remove: [
   ["rm" "-R" "%{lib}%/coq/user-contrib/mathcomp/contrib/grobner"]
   ["sh" "-c" "rmdir %{lib}%/coq/user-contrib/mathcomp/contrib || true"]
 ]
 depends: [
   "ocaml"
-  "coq" {>= "8.5"}
-  "coq-mathcomp-ssreflect" {>= "1.6"}
-  "coq-mathcomp-algebra"
-  "coq-mathcomp-multinomials" {= "1.6.dev"}
+  "coq" {>= "9.0" | = "dev"}
+  "coq-mathcomp-ssreflect" {>= "2.5.0"}
+  "coq-mathcomp-algebra" {>= "2.5.0"}
+  "coq-mathcomp-multinomials" {>= "2.4.0"}
 ]
-synopsis: "# grobner"
+synopsis: "Grobner basis"
 description: """
 A fornalisation of Grobner basis in ssreflect.
 It contains one file
@@ -28,15 +29,15 @@ grobner.v
 
 It defines.
 
-From mathcomp Require Import all_ssreflect all_algebra.
-From SsrMultinomials Require Import ssrcomplements poset freeg mpoly.
+From mathcomp Require Import all_boot all_algebra.
+From mathcomp Require Import ssrcomplements freeg mpoly.
 From mathcomp.contrib.grobner Require Import grobner.
 
 (* p belongs to the ideal generated by L *)
 
 Check ideal.
 
-ideal = 
+ideal =
 fun (R : ringType) (n : nat) (L : seq {mpoly R[n]}) (p : {mpoly R[n]})
   =>
   exists t, p = \\sum_(i < size L) t`_i * L`_i
@@ -51,6 +52,5 @@ idealfP
               (l : seq {mpoly R[n]}),
        reflect (ideal l p) (idealf l p)"""
 url {
-  src: "https://github.com/thery/grobner/archive/v1.0.1.zip"
-  checksum: "md5=ee88f5010096f45a5be120de58910913"
+  src: "git+https://github.com/thery/grobner.git#master"
 }
diff --git a/extra-dev/packages/coq-mod-red/coq-mod-red.dev/opam b/extra-dev/packages/coq-mod-red/coq-mod-red.dev/opam
index 57a857bf39..f0f65aa7fd 100644
--- a/extra-dev/packages/coq-mod-red/coq-mod-red.dev/opam
+++ b/extra-dev/packages/coq-mod-red/coq-mod-red.dev/opam
@@ -5,8 +5,8 @@ license: "GNU Lesser General Public License"
 build: [
   ["coq_makefile" "-f" "Make" "-o" "Makefile"]
   [make "-j%{jobs}%"]
-  [make "install"]
 ]
+install: [make "install"]
 remove: ["rm" "-R" "%{lib}%/coq/user-contrib/ModRed"]
 depends: [
   "ocaml"
diff --git a/extra-dev/packages/coq-qarith/coq-qarith.dev/opam b/extra-dev/packages/coq-qarith/coq-qarith.dev/opam
index 20f473795b..1082303982 100644
--- a/extra-dev/packages/coq-qarith/coq-qarith.dev/opam
+++ b/extra-dev/packages/coq-qarith/coq-qarith.dev/opam
@@ -5,8 +5,8 @@ license: "LGPL 2"
 build: [
   ["coq_makefile" "-f" "Make" "-o" "Makefile"]
   [make "-j%{jobs}%"]
-  [make "install"]
 ]
+install: [make "install"]
 remove: ["rm" "-R" "%{lib}%/coq/user-contrib/QArith"]
 depends: [
   "ocaml"
diff --git a/extra-dev/packages/coq-smc/coq-smc.dev/opam b/extra-dev/packages/coq-smc/coq-smc.dev/opam
index 1ab6b0f561..1257af7ed9 100644
--- a/extra-dev/packages/coq-smc/coq-smc.dev/opam
+++ b/extra-dev/packages/coq-smc/coq-smc.dev/opam
@@ -5,8 +5,8 @@ license: "LGPL 2"
 build: [
   ["coq_makefile" "-f" "Make" "-o" "Makefile"]
   [make "-j%{jobs}%"]
-  [make "install"]
 ]
+install: [make "install"]
 remove: ["rm" "-R" "%{lib}%/coq/user-contrib/SMC"]
 depends: [
   "ocaml"
diff --git a/extra-dev/packages/coq-zchinese/coq-zchinese.dev/opam b/extra-dev/packages/coq-zchinese/coq-zchinese.dev/opam
index 97bfd053aa..feb94db537 100644
--- a/extra-dev/packages/coq-zchinese/coq-zchinese.dev/opam
+++ b/extra-dev/packages/coq-zchinese/coq-zchinese.dev/opam
@@ -5,8 +5,8 @@ license: "Proprietary"
 build: [
   ["coq_makefile" "-f" "Make" "-o" "Makefile"]
   [make "-j%{jobs}%"]
-  [make "install"]
 ]
+install: [make "install"]
 remove: ["rm" "-R" "%{lib}%/coq/user-contrib/ZChinese"]
 depends: [
   "ocaml"
diff --git a/extra-dev/packages/coq-zsearch-trees/coq-zsearch-trees.dev/opam b/extra-dev/packages/coq-zsearch-trees/coq-zsearch-trees.dev/opam
index 9bcac62c32..44158f4df1 100644
--- a/extra-dev/packages/coq-zsearch-trees/coq-zsearch-trees.dev/opam
+++ b/extra-dev/packages/coq-zsearch-trees/coq-zsearch-trees.dev/opam
@@ -5,8 +5,8 @@ license: "LGPL 2"
 build: [
   ["coq_makefile" "-f" "Make" "-o" "Makefile"]
   [make "-j%{jobs}%"]
-  [make "install"]
 ]
+install: [make "install"]
 remove: ["rm" "-R" "%{lib}%/coq/user-contrib/ZSearchTrees"]
 depends: [
   "ocaml"