rocq-community · RalfJung · Aug 7, 2026 · Jul 16, 2026 · Aug 6, 2026 · Aug 6, 2026
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -1,4 +1,4 @@
-# This file was generated from `meta.yml`, please do not edit manually.
+# This file was generated from `meta.yml`, and then had to be edited manually.
 # Follow the instructions on https://github.com/coq-community/templates to regenerate.
 name: Docker CI
 
@@ -9,6 +9,7 @@ on:
   pull_request:
     branches:
       - '**'
+  workflow_dispatch:
 
 jobs:
   build:
@@ -17,19 +18,13 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp-dev:coq-dev'
-          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
-          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
-          - 'mathcomp/mathcomp:2.0.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.16.0-coq-8.17'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.16'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.14'
+          - 'mathcomp/mathcomp-dev:rocq-prover-dev'
+          - 'mathcomp/mathcomp:2.6.0-rocq-prover-9.2'
+          - 'mathcomp/mathcomp:2.6.0-rocq-prover-9.1'
+          - 'mathcomp/mathcomp:2.6.0-rocq-prover-9.0'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-autosubst-ci.opam'

diff --git a/Makefile b/Makefile
@@ -42,7 +42,7 @@ dist:
 
 doc: clean-doc manual.pdf
 	- mkdir -p $(DOC)
-	coqdoc $(COQDOCFLAGS) -R theories Autosubst -R examples/plain Plain \
+	rocq doc $(COQDOCFLAGS) -R theories Autosubst -R examples/plain Plain \
 	  -R examples/ssr Ssr $(THEORIES) $(EXAMPLES_PLAIN) $(EXAMPLES_SSR)
 	cp $(EXTRA_DIR)resources/* $(DOC)
 	cp manual.pdf $(DOC)

diff --git a/README.md b/README.md
@@ -1,5 +1,5 @@
 <!---
-This file was generated from `meta.yml`, please do not edit manually.
+This file was generated from `meta.yml`, and then had to be edited manually.
 Follow the instructions on https://github.com/coq-community/templates to regenerate.
 --->
 # Autosubst
@@ -10,8 +10,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![Zulip][zulip-shield]][zulip-link]
 [![DOI][doi-shield]][doi-link]
 
-[docker-action-shield]: https://github.com/coq-community/autosubst/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/coq-community/autosubst/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/autosubst/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/autosubst/actions/workflows/docker-action.yml
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -39,13 +39,13 @@ substitutions.
 - Author(s):
   - Steven Schäfer (initial)
   - Tobias Tebbi (initial)
-- Coq-community maintainer(s):
+- Rocq-community maintainer(s):
   - Ralf Jung ([**@RalfJung**](https://github.com/RalfJung))
   - Dan Frumin ([**@co-dan**](https://github.com/co-dan))
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: 8.14 or later
+- Compatible Rocq/Coq versions: 9.0 or later
 - Additional dependencies: none
-- Coq namespace: `Autosubst`
+- Rocq/Coq namespace: `Autosubst`
 - Related publication(s):
   - [Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions](https://www.ps.uni-saarland.de/Publications/documents/SchaeferEtAl_2015_Autosubst_-Reasoning.pdf) doi:[10.1007/978-3-319-22102-1_24](https://doi.org/10.1007/978-3-319-22102-1_24)
 
@@ -55,7 +55,7 @@ The easiest way to install the latest released version of Autosubst
 is via [OPAM](https://opam.ocaml.org/doc/Install.html):
 
 ```shell
-opam repo add coq-released https://coq.inria.fr/opam/released
+opam repo add rocq-released https://rocq-prover.org/opam/released
 opam install coq-autosubst
 ```
 

diff --git a/coq-autosubst-ci.opam b/coq-autosubst-ci.opam
@@ -11,6 +11,7 @@ synopsis: "Autosubst (CI only)"
 
 build: [make "-j%{jobs}%" "all"]
 depends: [
-  "coq"
-  "coq-mathcomp-ssreflect"
+  "rocq-core"
+  "rocq-stdlib"
+  "rocq-mathcomp-ssreflect"
 ]
diff --git a/coq-autosubst.opam b/coq-autosubst.opam
@@ -1,4 +1,4 @@
-# This file was generated from `meta.yml`, please do not edit manually.
+# This file was generated from `meta.yml`, and then had to be edited manually.
 # Follow the instructions on https://github.com/coq-community/templates to regenerate.
 
 opam-version: "2.0"
@@ -23,7 +23,8 @@ substitutions."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.14" & < "8.21~") | (= "dev")}
+    "rocq-core"
+    "rocq-stdlib"
 ]
 
 tags: [

diff --git a/examples/plain/Makefile b/examples/plain/Makefile
@@ -8,7 +8,7 @@ all: $(COQMAKEFILE)
 	+$(MAKE) -f $(COQMAKEFILE) all
 
 $(COQMAKEFILE): Makefile $(VS)
-	coq_makefile -R $(LIB) Autosubst -R . Plain $(VS) -o $(COQMAKEFILE)
+	rocq makefile -R $(LIB) Autosubst -R . Plain $(VS) -o $(COQMAKEFILE)
 
 clean: $(COQMAKEFILE)
 	-$(COQMAKE) clean

diff --git a/examples/ssr/Makefile b/examples/ssr/Makefile
@@ -8,7 +8,7 @@ all: $(COQMAKEFILE)
 	+$(MAKE) -f $(COQMAKEFILE) all
 
 $(COQMAKEFILE): Makefile $(VS)
-	coq_makefile -R $(LIB) Autosubst $(VS) -R . Ssr -o $(COQMAKEFILE)
+	rocq makefile -R $(LIB) Autosubst $(VS) -R . Ssr -o $(COQMAKEFILE)
 
 clean: $(COQMAKEFILE)
 	-$(COQMAKE) clean

diff --git a/meta.yml b/meta.yml
@@ -46,29 +46,17 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: 8.14 or later
-  opam: '{(>= "8.14" & < "8.21~") | (= "dev")}'
+  text: 9.0 or later
+  opam: '{(>= "9.0") | (= "dev")}'
 
 tested_coq_opam_versions:
-- version: 'coq-dev'
+- version: 'rocq-prover-dev'
   repo: 'mathcomp/mathcomp-dev'
-- version: '2.2.0-coq-8.19'
+- version: '2.6.0-rocq-prover-9.2'
   repo: 'mathcomp/mathcomp'
-- version: '2.1.0-coq-8.18'
+- version: '2.6.0-rocq-prover-9.1'
   repo: 'mathcomp/mathcomp'
-- version: '2.0.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '1.17.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '1.16.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.15'
-  repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.15'
-  repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.14'
+- version: '2.6.0-rocq-prover-9.0'
   repo: 'mathcomp/mathcomp'
 
 namespace: Autosubst

diff --git a/theories/Makefile b/theories/Makefile
@@ -8,7 +8,7 @@ all: $(COQMAKEFILE)
 	+$(MAKE) -f $(COQMAKEFILE) all
 
 $(COQMAKEFILE): Makefile $(VS)
-	coq_makefile -R $(LIB) Autosubst $(VS) -o $(COQMAKEFILE)
+	rocq makefile -R $(LIB) Autosubst $(VS) -o $(COQMAKEFILE)
 
 install: $(COQMAKEFILE)
 	$(COQMAKE) install