diff --git a/.github/workflows/coq-alpine.yml b/.github/workflows/coq-alpine.yml
index e38e3a2d6..79b265efc 100644
--- a/.github/workflows/coq-alpine.yml
+++ b/.github/workflows/coq-alpine.yml
@@ -25,7 +25,7 @@ jobs:
     name: alpine-${{ matrix.alpine }}
 
     concurrency:
-      group: ${{ github.workflow }}-alpine-${{ matrix.alpine }}-${{ github.head_ref || github.run_id }}
+      group: ${{ github.workflow }}-alpine-${{ matrix.alpine }}-${{ github.event.pull_request.number || github.head_ref || github.run_id }}
       cancel-in-progress: true
 
     steps:
diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml
index 85115eee9..8330bdd2a 100644
--- a/.github/workflows/coq-debian.yml
+++ b/.github/workflows/coq-debian.yml
@@ -25,7 +25,7 @@ jobs:
     container: debian:${{ matrix.debian }}
 
     concurrency:
-      group: ${{ github.workflow }}-debian-${{ matrix.debian }}-${{ github.head_ref || github.run_id }}
+      group: ${{ github.workflow }}-debian-${{ matrix.debian }}-${{ github.event.pull_request.number || github.head_ref || github.run_id }}
       cancel-in-progress: true
 
     steps:
diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml
index f83e33d34..89d3ccc69 100644
--- a/.github/workflows/coq-docker.yml
+++ b/.github/workflows/coq-docker.yml
@@ -17,7 +17,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        coq-version: [ '8.19', '8.20' , '9.0' , '9.1' ]
+        coq-version: [ '9.0' , '9.1' , '9.2' ]
         extra-gh-reportify: [ '' ]
         skip-validate: [ '' ]
         include:
@@ -29,7 +29,7 @@ jobs:
     name: ${{ matrix.coq-version }}
 
     concurrency:
-      group: ${{ github.workflow }}-${{ matrix.coq-version }}-${{ github.head_ref || github.run_id }}
+      group: ${{ github.workflow }}-${{ matrix.coq-version }}-${{ github.event.pull_request.number || github.head_ref || github.run_id }}
       cancel-in-progress: true
 
     steps:
@@ -49,7 +49,6 @@ jobs:
           sudo apt-get update -y
           sudo apt-get install -y python-is-python3 python3
           eval $(opam env)
-          opam install coq -y
           echo '::endgroup::'
           echo '::remove-matcher owner=coq-problem-matcher::'
           CI=1 etc/ci/describe-system-config.sh
@@ -78,7 +77,6 @@ jobs:
           sudo apt-get update -y
           sudo apt-get install -y python-is-python3 python3
           eval $(opam env)
-          opam install coq -y
           echo '::endgroup::'
           echo '::remove-matcher owner=coq-problem-matcher::'
           etc/ci/github-actions-make.sh TIMED=1 validate COQCHKFLAGS="-o"
diff --git a/.github/workflows/coq-opam-package.yml b/.github/workflows/coq-opam-package.yml
index f237699f1..dc00d1235 100644
--- a/.github/workflows/coq-opam-package.yml
+++ b/.github/workflows/coq-opam-package.yml
@@ -17,7 +17,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        coq-version: ['dev', '8.20.0', '8.19.0', '9.0.0' , '9.1.0' ]
+        coq-version: ['dev', '9.0.0', '9.1.0', '9.2.0']
         os: [{name: 'Ubuntu',
               runs-on: 'ubuntu-latest',
               ocaml-compiler: '4.14.0',
@@ -127,14 +127,14 @@ jobs:
         echo ::group::opam list
         opam list
         echo ::endgroup::
-        echo ::group::coqc --config
-        opam exec -- coqc --config
+        echo ::group::rocq --config
+        opam exec -- rocq --config
         echo ::endgroup::
-        echo ::group::coqc --version
-        opam exec -- coqc --version
+        echo ::group::rocq --version
+        opam exec -- rocq --version
         echo ::endgroup::
-        echo ::group::echo ~ coqtop
-        echo "" | opam exec -- coqtop
+        echo ::group::echo ~ rocq top
+        echo "" | opam exec -- rocq top
         echo ::endgroup::
 
     - run: opam install coq-rewriter ${{ matrix.os.opam-jobs-flag }}
diff --git a/Makefile b/Makefile
index 48e7275d2..8fa80daac 100644
--- a/Makefile
+++ b/Makefile
@@ -81,7 +81,7 @@ endif
 # We must work around COQBUG(https://github.com/coq/coq/issues/10907) and fix the conf target
 Makefile.coq Makefile-old.conf: Makefile _CoqProject $(COQ_VERSION_FILE)
 	$(SHOW)'COQ_MAKEFILE -f _CoqProject > Makefile.coq'
-	$(HIDE)(($(COQBIN)coq_makefile -f _CoqProject -o Makefile-old && cat Makefile-old | sed s'/Makefile-old.conf:/Makefile-old-old.conf:/g' | sed 's/Makefile-old.local/Makefile.local/g; s/^-\?include Makefile.local-late$$//g' $(EXTRA_SED_FOR_DEPS)); echo; echo 'include Makefile.local-late') > Makefile.coq && rm Makefile-old
+	$(HIDE)(("$(COQBIN)rocq" makefile -f _CoqProject -o Makefile-old && cat Makefile-old | sed s'/Makefile-old.conf:/Makefile-old-old.conf:/g' | sed 's/Makefile-old.local/Makefile.local/g; s/^-\?include Makefile.local-late$$//g' $(EXTRA_SED_FOR_DEPS)); echo; echo 'include Makefile.local-late') > Makefile.coq && rm Makefile-old
 
 Makefile.coq: | Makefile-old.conf
 
diff --git a/Makefile.local.common b/Makefile.local.common
index 7556c3ac9..5ca8e7b1d 100644
--- a/Makefile.local.common
+++ b/Makefile.local.common
@@ -18,14 +18,16 @@ TIMECMD_FULL?=
 TIMER_FULL=$(if $(TIMED), $(STDTIME_FULL), $(TIMECMD_FULL))
 
 COQ_VERSION_FILE = .coq-version
-COQ_VERSION_PREFIX = The Coq Proof Assistant, version
 ROCQ_VERSION_PREFIX = The Rocq Prover, version
-COQ_VERSION_COQTOP_CMD := $(COQBIN)coqtop </dev/null
-COQ_VERSION_COQC_CMD := $(COQBIN)coqc --version
-COQC_VERSION_FULL := $(shell $(COQ_VERSION_COQC_CMD) 2>/dev/null)
-COQ_VERSION := $(firstword $(subst $(ROCQ_VERSION_PREFIX),,$(subst $(COQ_VERSION_PREFIX),,$(COQC_VERSION_FULL))))
+COQ_VERSION_PREFIX = The Coq Proof Assistant, version
+ROCQ ?= "$(COQBIN)rocq"
+COQ_VERSION_COQTOP_CMD := $(ROCQ) top </dev/null
+COQ_VERSION_COQC_CMD := $(ROCQ) --version
+ROCQ_VERSION_FULL := $(shell $(COQ_VERSION_COQC_CMD) 2>/dev/null)
+COQC_VERSION_FULL := $(ROCQ_VERSION_FULL)
+COQ_VERSION := $(firstword $(subst $(ROCQ_VERSION_PREFIX),,$(subst $(COQ_VERSION_PREFIX),,$(ROCQ_VERSION_FULL))))
 
-COQ_EXTENDED_VERSION:=$(strip $(shell $(COQ_VERSION_COQTOP_CMD) 2>/dev/null) $(COQC_VERSION_FULL))
+COQ_EXTENDED_VERSION:=$(strip $(shell $(COQ_VERSION_COQTOP_CMD) 2>/dev/null) $(ROCQ_VERSION_FULL))
 COQ_EXTENDED_VERSION_OLD:=$(strip $(shell cat $(COQ_VERSION_FILE) 2>/dev/null))
 
 # Extract "major.minor" robustly from version strings like "9.2", "9.2.0",
diff --git a/coq-rewriter.opam b/coq-rewriter.opam
index a8496545b..6ed78cd19 100644
--- a/coq-rewriter.opam
+++ b/coq-rewriter.opam
@@ -15,8 +15,9 @@ build: [
 install: [make "install"]
 depends: [
   "conf-findutils" {build}
-  "ocaml" {build & (arch = "x86_32" | arch = "x86_64" | >= "4.14.0")}
-  "coq" {>= "8.19~"}
+  "ocaml"
+  "rocq-core" {>= "9.0~"}
+  "rocq-stdlib" {>= "9.0~"}
 ]
 dev-repo: "git+https://github.com/mit-plv/rewriter.git"
 synopsis: "Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting, experimental and tailored for use in Fiat Cryptography"
diff --git a/etc/ci/describe-system-config.sh b/etc/ci/describe-system-config.sh
index 0bfad6121..1918b29c2 100755
--- a/etc/ci/describe-system-config.sh
+++ b/etc/ci/describe-system-config.sh
@@ -53,9 +53,9 @@ group ocamlfind query rocq-runtime
 group ocamlfind query rocq-runtime.plugins
 group ocamlfind query rocq-runtime.plugins.ltac
 group "ocamlfind query coq | xargs find"
-group coqc --config
-group coqc --version
-group "true | coqtop"
+group rocq --config
+group rocq --version
+group "true | rocq top"
 group etc/machine.sh
 group "echo PATH=$PATH"
 group "echo SHELL=$SHELL"
diff --git a/etc/ci/github-actions-make.sh b/etc/ci/github-actions-make.sh
index 20526d297..d4c3fa70d 100755
--- a/etc/ci/github-actions-make.sh
+++ b/etc/ci/github-actions-make.sh
@@ -20,7 +20,7 @@ if [ "$1" == "--warnings" ]; then
     shift
 fi
 if [ ! -z "${reportify}" ]; then
-    reportify="COQC='$(pwd)/etc/coq-scripts/github/reportify-coq.sh'${reportify} ${COQBIN}coqc"
+    reportify="COQC='$(pwd)/etc/coq-scripts/github/reportify-coq.sh'${reportify} ${COQBIN}rocq compile"
 fi
 
 rm -f finished.ok
diff --git a/src/Rewriter/Rewriter/Examples/PerfTesting/Makefile.coq-versions-lite b/src/Rewriter/Rewriter/Examples/PerfTesting/Makefile.coq-versions-lite
index 5f443c321..97cbe842f 100644
--- a/src/Rewriter/Rewriter/Examples/PerfTesting/Makefile.coq-versions-lite
+++ b/src/Rewriter/Rewriter/Examples/PerfTesting/Makefile.coq-versions-lite
@@ -10,10 +10,10 @@ COQ_VERSION_SHORT_DATE_FILE = .coq-version-short-date
 COQ_VERSION_CONFIG_FILE := .coq-version-config
 COQ_VERSION_OCAML_VERSION_FILE := .coq-version-ocaml-version
 COQ_VERSION_OCAML_CONFIG_FILE := .coq-version-ocaml-config
-COQ_VERSION_PREFIX = The Coq Proof Assistant, version
-COQ_VERSION_FULL := $(subst $(COQ_VERSION_PREFIX),,$(shell $(COQBIN)coqc --version 2>/dev/null))
+COQ_VERSION_PREFIX = The Rocq Prover, version
+COQ_VERSION_FULL := $(subst $(COQ_VERSION_PREFIX),,$(shell "$(COQBIN)rocq" --version 2>/dev/null))
 COQ_VERSION := $(firstword $(COQ_VERSION_FULL))
-COQ_VERSION_CONFIG_CMD = $(COQBIN)coqc -config 2>/dev/null
+COQ_VERSION_CONFIG_CMD = "$(COQBIN)rocq" compile -config 2>/dev/null
 COQ_VERSION_DATE := $(subst $(OPEN_PAREN),,$(subst $(CLOSE_PAREN),,$(wordlist 2, 3, $(COQ_VERSION_FULL))))
 COQ_VERSION_COMPILATION := $(subst $(JOINER)with,$(SPACE)with,$(subst $(SPACE),$(JOINER),$(wordlist 4, $(words $(COQ_VERSION_FULL)),$(COQ_VERSION_FULL))))
 COQ_VERSION_COMPILATION_DATE := $(subst $(JOINER),$(SPACE),$(subst compiled$(JOINER)on$(JOINER),,$(firstword $(COQ_VERSION_COMPILATION))))
@@ -23,7 +23,7 @@ VERSION_FILES := $(COQ_VERSION_FILE) $(COQ_VERSION_SHORT_FILE) $(COQ_VERSION_SHO
 MACHINE_FILE = .machine
 MACHINE_EXTENDED_FILE = .machine-extended
 
-COQ_EXTENDED_VERSION := $(shell (true | $(COQBIN)coqtop 2>/dev/null; $(COQBIN)coqc --version 2>/dev/null))
+COQ_EXTENDED_VERSION := $(shell (true | "$(COQBIN)rocq" top 2>/dev/null; "$(COQBIN)rocq" --version 2>/dev/null))
 COQ_EXTENDED_VERSION_OLD := $(shell cat $(COQ_VERSION_FILE) 2>/dev/null)
 
 HAS_LTAC2:=