diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 78e2086..49e2c8e 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -18,14 +18,16 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.4.0-coq-8.20'
           - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
           - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.1'
-          - 'mathcomp/mathcomp:2.5.0-coq-8.20'
           - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.0'
           - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.1'
+          - 'mathcomp/mathcomp:2.6.0-rocq-prover-9.0'
+          - 'mathcomp/mathcomp:2.6.0-rocq-prover-9.1'
+          - 'mathcomp/mathcomp:2.6.0-rocq-prover-9.2'
           - 'mathcomp/mathcomp-dev:rocq-prover-9.0'
           - 'mathcomp/mathcomp-dev:rocq-prover-9.1'
+          - 'mathcomp/mathcomp-dev:rocq-prover-9.2'
           - 'mathcomp/mathcomp-dev:rocq-prover-dev'
       fail-fast: false
     steps:
diff --git a/Makefile b/Makefile
index 3964aef..8b62c7a 100644
--- a/Makefile
+++ b/Makefile
@@ -9,7 +9,7 @@ KNOWNFILES   := Makefile Make Make.test-suite
 
 .DEFAULT_GOAL := invoke-coqmakefile
 
-COQMAKEFILE       = $(COQBIN)coq_makefile
+COQMAKEFILE       = $(COQBIN)rocq makefile
 COQMAKE           = $(MAKE) --no-print-directory -f Makefile.coq
 COQMAKE_TESTSUITE = $(MAKE) --no-print-directory -f Makefile.test-suite.coq
 
diff --git a/Makefile.coq.local b/Makefile.coq.local
deleted file mode 100644
index 9dbdb16..0000000
--- a/Makefile.coq.local
+++ /dev/null
@@ -1,7 +0,0 @@
-pre-all::
-	if command -v coqc > /dev/null && (coqc --version | grep -q '8.18\|8.19\|8.20') ; then \
-	  for f in $(shell grep "From Stdlib" $$(find . -name "*.v") | cut -d: -f1) ; do \
-	    sed -i.bak 's/From Stdlib/From Coq/' $${f} ; \
-	    $(RM) $${f}.bak ; \
-	  done ; \
-	fi
diff --git a/README.md b/README.md
index 7dc6eaa..48ea7f1 100644
--- a/README.md
+++ b/README.md
@@ -21,8 +21,9 @@ by extending the zify tactic.
 - Author(s):
   - Kazuhiko Sakaguchi (initial)
 - License: [CeCILL-B Free Software License Agreement](CeCILL-B)
-- Compatible Rocq/Coq versions: 8.20 or later
+- Compatible Rocq/Coq versions: 9.0 or later
 - Additional dependencies:
+  - Rocq standard library
   - [MathComp](https://math-comp.github.io) ssreflect 2.4 or later
   - [MathComp](https://math-comp.github.io) algebra
 - Rocq/Coq namespace: `mathcomp.zify`
diff --git a/meta.yml b/meta.yml
index 19c9ed4..c71691d 100644
--- a/meta.yml
+++ b/meta.yml
@@ -25,32 +25,40 @@ license:
   file: CeCILL-B
 
 supported_coq_versions:
-  text: 8.20 or later
-  opam: '{>= "8.20"}'
+  text: 9.0 or later
+  opam: '{>= "9.0"}'
 
 tested_coq_nix_versions:
 
 tested_coq_opam_versions:
-- version: '2.4.0-coq-8.20'
-  repo: 'mathcomp/mathcomp'
 - version: '2.4.0-rocq-prover-9.0'
   repo: 'mathcomp/mathcomp'
 - version: '2.4.0-rocq-prover-9.1'
   repo: 'mathcomp/mathcomp'
-- version: '2.5.0-coq-8.20'
-  repo: 'mathcomp/mathcomp'
 - version: '2.5.0-rocq-prover-9.0'
   repo: 'mathcomp/mathcomp'
 - version: '2.5.0-rocq-prover-9.1'
   repo: 'mathcomp/mathcomp'
+- version: '2.6.0-rocq-prover-9.0'
+  repo: 'mathcomp/mathcomp'
+- version: '2.6.0-rocq-prover-9.1'
+  repo: 'mathcomp/mathcomp'
+- version: '2.6.0-rocq-prover-9.2'
+  repo: 'mathcomp/mathcomp'
 - version: 'rocq-prover-9.0'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'rocq-prover-9.1'
   repo: 'mathcomp/mathcomp-dev'
+- version: 'rocq-prover-9.2'
+  repo: 'mathcomp/mathcomp-dev'
 - version: 'rocq-prover-dev'
   repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
+- opam:
+    name: rocq-stdlib
+  description: |-
+    Rocq standard library
 - opam:
     name: rocq-mathcomp-ssreflect
     version: '{>= "2.4"}'
diff --git a/rocq-mathcomp-zify.opam b/rocq-mathcomp-zify.opam
index 421c242..d2e7ab4 100644
--- a/rocq-mathcomp-zify.opam
+++ b/rocq-mathcomp-zify.opam
@@ -20,7 +20,8 @@ build: [make "-j%{jobs}%"]
 run-test: [make "-j%{jobs}%" "test-suite"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.20"}
+  "rocq-core" {>= "9.0"}
+  "rocq-stdlib" 
   "rocq-mathcomp-ssreflect" {>= "2.4"}
   "rocq-mathcomp-algebra" 
 ]