thibautbenjamin · thibautbenjamin · Mar 24, 2026 · Oct 1, 2025 · Oct 1, 2025 · Oct 1, 2025
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -9,5 +9,5 @@ jobs:
       with:
         github_access_token: ${{ secrets.GITHUB_TOKEN }}
     - run: nix build
-    - run: nix build ./.#catt-coq-plugin
-    - run: nix flake check --all-systems
+    - run: nix build ./.#catt-rocq-plugin
+    - run: nix flake check --all-systems
diff --git a/README.md b/README.md
@@ -17,9 +17,9 @@ Make sure `opam` is installed, clone the project and move to the directory where
 ```
 opam install ./catt.opam
 ```
-The Coq plugin can be installed with the following command
+The Rocq plugin can be installed with the following command
 ```
-opam install ./coq-catt-plugin.opam
+opam install ./rocq-catt-plugin.opam
 ```
 
 ### Building from source with dune and opam
@@ -31,15 +31,15 @@ opam install --deps-only ./catt.opam
 dune build catt.install
 ```
 
-To build the Coq plugin, run the following commands:
+To build the Rocq plugin, run the following commands:
 ```
-opam install --deps-only ./coq-catt-plugin.opam
-dune build coq-catt-plugin.install
+opam install --deps-only ./rocq-catt-plugin.opam
+dune build rocq-catt-plugin.install
 ```
 
 ### Using nix
 
-This repository contains a `flake.nix` file that defines the packages `catt` and `coq-catt-plugin`, as well as `catt-mode`, an editing mode for catt in emacs.
+This repository contains a `flake.nix` file that defines the packages `catt` and `rocq-catt-plugin`, as well as `catt-mode`, an editing mode for catt in emacs.
 
 ## Syntax
 There are two keywords to define a new operation:
@@ -281,16 +281,16 @@ Calling `catt --no-builtin [FILE]` will deactivate the use of the built-in ident
 Calling `catt --keep-going [FILE]` will make it so that `catt` will report errors but will keep running on the file and exit with a success even if the file does not typecheck properly. This is not the default behaviour, as in a typical use case, later definitions depend on earlier ones, so if a defined coherence or term is invalid, all further coherences and terms depending on it also fail. This option is useful for scripting and testing.
 
 
-## Coq plugin
-`catt` also provide a plugin for the proof assistant `coq` (packaged separately, called `coq-catt-plugin`), that allows one to export any defined term in `catt` into a function computing higher identity witnesses in `coq`. Once the plugin is installed, write the following to load it at the head of a `coq` file:
+## Rocq plugin
+`catt` also provide a plugin for the proof assistant `rocq` (packaged separately, called `rocq-catt-plugin`), that allows one to export any defined term in `catt` into a function computing higher identity witnesses in `rocq`. Once the plugin is installed, write the following to load it at the head of a `rocq` file:
 ```
 From Catt Require Import Loader.
 ```
-You can then use the `Catt` command in `coq` as follows:
+You can then use the `Catt` command in `rocq` as follows:
 ```
 Catt [NAMES] FROM FILE [PATH].
 ```
-where `[NAMES]` is a list of names of `catt` terms and `[PATH]` is a file containing the definition of those `catt` terms. Upon evaluation of this line, `coq` will call `catt` on the given file and export the listed terms into `coq` terms, whose names will be given as `catt_[NAME]`. For instance, one can write the following:
+where `[NAMES]` is a list of names of `catt` terms and `[PATH]` is a file containing the definition of those `catt` terms. Upon evaluation of this line, `rocq` will call `catt` on the given file and export the listed terms into `rocq` terms, whose names will be given as `catt_[NAME]`. For instance, one can write the following:
 ```
 Catt "whiskr" From File "../example/file.catt".
 

diff --git a/catt.opam b/catt.opam
@@ -16,7 +16,7 @@ homepage: "https://github.com/thibautbenjamin/catt"
 bug-reports: "https://github.com/thibautbenjamin/catt/issues"
 depends: [
   "ocaml" {>= "4.14" & < "5.0"}
-  "dune" {>= "3.16" & >= "3.10"}
+  "dune" {>= "3.20" & >= "3.10"}
   "menhir" {>= "20240715"}
   "base" {>= "0.17.0"}
   "odoc" {with-doc}
@@ -36,3 +36,4 @@ build: [
   ]
 ]
 dev-repo: "git+https://github.com/thibautbenjamin/catt.git"
+x-maintenance-intent: ["(latest)"]
diff --git a/coq-catt-plugin.opam b/coq-catt-plugin.opam
@@ -1,8 +1,8 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-synopsis: "A Coq plugin for the catt proof-assistant"
+synopsis: "A Rocq plugin for the catt proof-assistant"
 description:
-  "A Coq plugin to interpret terms built in the catt proof assistant as functions computing on higher dimensional identity types"
+  "A Rocq plugin to interpret terms built in the catt proof assistant as functions computing on higher dimensional identity types"
 maintainer: [
   "Thibaut Benjamin <thibaut.benjamin@gmail.com>"
   "Chiara Sarti  <cs2197@cam.ac.uk>"
@@ -16,9 +16,9 @@ tags: ["higher-categories" "dependent-type-theory"]
 homepage: "https://github.com/thibautbenjamin/catt"
 bug-reports: "https://github.com/thibautbenjamin/catt/issues"
 depends: [
-  "dune" {>= "3.16"}
+  "dune" {>= "3.20"}
   "catt"
-  "coq" {>= "8.20"}
+  "coq" {>= "9.0"}
   "odoc" {with-doc}
 ]
 build: [
@@ -36,3 +36,4 @@ build: [
   ]
 ]
 dev-repo: "git+https://github.com/thibautbenjamin/catt.git"
+x-maintenance-intent: ["(latest)"]
diff --git a/dune-project b/dune-project
@@ -1,4 +1,4 @@
-(lang dune 3.16)
+(lang dune 3.20)
 
 (name catt)
 (generate_opam_files true)
@@ -10,7 +10,7 @@
 (license MIT)
 (using menhir 2.0)
 (cram enable)
-(using coq 0.9)
+(using coq 0.10)
 
 (package
   (name catt)
@@ -26,11 +26,11 @@
 
 (package
   (name coq-catt-plugin)
-  (synopsis "A Coq plugin for the catt proof-assistant")
-  (description "A Coq plugin to interpret terms built in the catt proof assistant as functions computing on higher dimensional identity types")
+  (synopsis "A Rocq plugin for the catt proof-assistant")
+  (description "A Rocq plugin to interpret terms built in the catt proof assistant as functions computing on higher dimensional identity types")
   (depends
       catt
-      (coq (>= 8.20)))
+      (coq (>= 9.0)))
   (tags
     (higher-categories dependent-type-theory)))
 

diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -7,8 +7,16 @@
     nix-filter.url = "github:numtide/nix-filter";
   };
 
-  outputs = { self, nixpkgs, flake-utils, nix-filter, ... }:
-    flake-utils.lib.eachDefaultSystem (system:
+  outputs =
+    {
+      self,
+      nixpkgs,
+      flake-utils,
+      nix-filter,
+      ...
+    }:
+    flake-utils.lib.eachDefaultSystem (
+      system:
       let
         pkgs = (import nixpkgs { inherit system; });
         ocamlPackages = pkgs.ocaml-ng.ocamlPackages_4_14;
@@ -33,12 +41,12 @@
             ];
           };
 
-          coq-plugin = nix-filter.lib {
+          rocq-plugin = nix-filter.lib {
             root = ./.;
             include = [
               ".ocamlformat"
               "dune-project"
-              (nix-filter.lib.inDirectory "coq_plugin")
+              (nix-filter.lib.inDirectory "rocq_plugin")
               (nix-filter.lib.inDirectory "test.t")
             ];
           };
@@ -52,8 +60,8 @@
               (nix-filter.lib.inDirectory "lib")
               (nix-filter.lib.inDirectory "test.t")
               (nix-filter.lib.inDirectory "web")
-              (nix-filter.lib.inDirectory "coq_plugin/src/")
-              "coq_plugin/theories/dune"
+              (nix-filter.lib.inDirectory "rocq_plugin/src/")
+              "rocq_plugin/theories/dune"
             ];
           };
 
@@ -65,7 +73,8 @@
           elisp = ./share/site-lisp;
         };
 
-      in {
+      in
+      {
         packages = {
           default = self.packages.${system}.catt;
 
@@ -85,7 +94,10 @@
               description = "A proof assistant for weak omega-categories";
               homepage = "https://www.github.com/thibautbenjamin/catt";
               license = nixpkgs.lib.licenses.mit;
-              maintainers = [ "Thibaut Benjamin" "Chiara Sarti" ];
+              maintainers = [
+                "Thibaut Benjamin"
+                "Chiara Sarti"
+              ];
               mainProgram = "catt";
             };
           };
@@ -107,30 +119,39 @@
             ];
 
             meta = {
-              description =
-                "Browser embedded version of the catt proof-assistant";
+              description = "Browser embedded version of the catt proof-assistant";
               homepage = "https://www.github.com/thibautbenjamin/catt";
               license = nixpkgs.lib.licenses.mit;
-              maintainers = [ "Thibaut Benjamin" "Chiara Sarti" ];
+              maintainers = [
+                "Thibaut Benjamin"
+                "Chiara Sarti"
+              ];
             };
           };
 
-          catt-coq-plugin = pkgs.coqPackages.mkCoqDerivation {
+          catt-rocq-plugin = pkgs.coqPackages.mkCoqDerivation {
             pname = "catt-plugin";
             version = "1.0";
-            src = sources.coq-plugin;
+            src = sources.rocq-plugin;
             nativeBuildInputs = [ ];
 
-            buildInputs =
-              [ self.packages.${system}.catt pkgs.dune_3 pkgs.opam pkgs.coq ];
+            buildInputs = [
+              self.packages.${system}.catt
+              pkgs.dune_3
+              pkgs.opam
+              pkgs.rocq-core
+            ];
             mlPlugin = true;
             useDune = true;
 
             meta = {
-              description = "Coq plugin for the catt proof-assistant";
+              description = "Rocq plugin for the catt proof-assistant";
               homepage = "https://www.github.com/thibautbenjamin/catt";
               license = nixpkgs.lib.licenses.mit;
-              maintainers = [ "Thibaut Benjamin" "Chiara Sarti" ];
+              maintainers = [
+                "Thibaut Benjamin"
+                "Chiara Sarti"
+              ];
             };
           };
 
@@ -148,30 +169,36 @@
           };
         };
 
-        formatter = pkgs.nixfmt-classic;
+        formatter = pkgs.nixfmt;
 
         checks = {
-          lint-nix = pkgs.runCommand "check-flake-format" {
-            nativeBuildInputs = [ pkgs.nixfmt-classic ];
-          } ''
-            echo "checking nix formatting"
-            nixfmt --check ${sources.nix}
-            touch $out
-          '';
-
-          dune-fmt = pkgs.runCommand "check-ocaml-fmt" {
-            nativeBuildInputs = [
-              ocamlPackages.dune_3
-              ocamlPackages.ocaml
-              ocamlPackages.ocamlformat
-            ];
-          } ''
-            echo "checking dune and ocaml formatting for catt"
-            dune fmt \
-                  --display=short \
-                  --root=$(pwd)
-                  touch $out
-          '';
+          lint-nix =
+            pkgs.runCommand "check-flake-format"
+              {
+                nativeBuildInputs = [ pkgs.nixfmt ];
+              }
+              ''
+                echo "checking nix formatting"
+                nixfmt --check ${sources.nix}
+                touch $out
+              '';
+
+          dune-fmt =
+            pkgs.runCommand "check-ocaml-fmt"
+              {
+                nativeBuildInputs = [
+                  ocamlPackages.dune_3
+                  ocamlPackages.ocaml
+                  ocamlPackages.ocamlformat
+                ];
+              }
+              ''
+                echo "checking dune and ocaml formatting for catt"
+                dune fmt \
+                      --display=short \
+                      --root=$(pwd)
+                      touch $out
+              '';
 
           default = self.packages.${system}.catt.overrideAttrs (oldAttrs: {
             name = "check-${oldAttrs.name}";
@@ -181,7 +208,11 @@
         };
 
         devShells.default = pkgs.mkShell {
-          packages = (with pkgs; [ nixfmt-classic fswatch ])
+          packages =
+            (with pkgs; [
+              nixfmt
+              fswatch
+            ])
             ++ (with ocamlPackages; [
               odoc
               ocaml-lsp
@@ -197,10 +228,11 @@
           inputsFrom = [
             self.packages.${system}.catt
             self.packages.${system}.catt-web
-            self.packages.${system}.catt-coq-plugin
+            self.packages.${system}.catt-rocq-plugin
           ];
         };
 
         devShells.web = self.packages.${system}.catt-web;
-      });
+      }
+    );
 }
diff --git a/coq_plugin/_CoqProject → rocq_plugin/_CoqProject b/coq_plugin/_CoqProject → rocq_plugin/_CoqProject
@@ -1,3 +1,3 @@
 -generate-meta-for-package catt
--R ../_build/default/coq_plugin/theories/ Catt
+-R ../_build/default/rocq_plugin/theories/ Catt
 -I ../_build/install/default/lib/
diff --git a/coq_plugin/src/coq_plugin.mlpack → rocq_plugin/src/coq_plugin.mlpack b/coq_plugin/src/coq_plugin.mlpack → rocq_plugin/src/coq_plugin.mlpack
diff --git a/coq_plugin/src/dune → rocq_plugin/src/dune b/coq_plugin/src/dune → rocq_plugin/src/dune