From ddb1144d7a2a8bc5114fcea2454aab290ca4f15a Mon Sep 17 00:00:00 2001
From: Serhii Khoma <sergey@nordicresults.com>
Date: Wed, 22 Jul 2026 20:57:16 +0700
Subject: [PATCH 1/8] feat: update to latest rocq -> nix check passes

---
 .gitmodules                  |  0
 Makefile                     |  2 +-
 docker_image/Dockerfile      |  8 +++---
 exercises/array_lock.v       | 15 ++++++-----
 exercises/custom_ra.v        |  2 +-
 exercises/gr_predicates.v    |  2 +-
 exercises/ofe.v              | 14 +++++++---
 exercises/resource_algebra.v | 16 ++++++------
 flake.lock                   | 27 +++++++++++++++++++
 flake.nix                    | 50 ++++++++++++++++++++++++++++++++++++
 iris-tutorial.opam           |  8 +++---
 theories/array_lock.v        | 15 ++++++-----
 theories/custom_ra.v         |  4 +--
 theories/gr_predicates.v     |  2 +-
 theories/ofe.v               | 16 +++++++++---
 theories/resource_algebra.v  | 16 ++++++------
 16 files changed, 148 insertions(+), 49 deletions(-)
 delete mode 100644 .gitmodules
 create mode 100644 flake.lock
 create mode 100644 flake.nix

diff --git a/.gitmodules b/.gitmodules
deleted file mode 100644
index e69de29..0000000
diff --git a/Makefile b/Makefile
index 550e378..f80f881 100644
--- a/Makefile
+++ b/Makefile
@@ -24,7 +24,7 @@ html: Makefile.coq _CoqProject
 .PHONY: html
 
 Makefile.coq: _CoqProject
-	coq_makefile -f _CoqProject -o Makefile.coq
+	rocq makefile -f _CoqProject -o Makefile.coq
 
 exercises: $(EXERCISES)
 .PHONY: exercises
diff --git a/docker_image/Dockerfile b/docker_image/Dockerfile
index 1134074..646fa45 100644
--- a/docker_image/Dockerfile
+++ b/docker_image/Dockerfile
@@ -19,14 +19,14 @@ RUN opam repo add --set-default iris-dev https://gitlab.mpi-sws.org/iris/opam.gi
 RUN opam switch create stable ocaml.5.2.0
 RUN eval $(opam env)
 RUN opam update
-RUN opam install coq.8.20.1 vscoq-language-server
-RUN opam install coq-iris.4.3.0 coq-iris-heap-lang
+RUN opam install rocq-core.9.1.1 vsrocq-language-server
+RUN opam install rocq-iris.4.5.0 rocq-iris-heap-lang
 
 RUN opam switch create unstable ocaml.5.2.0
 RUN eval $(opam env)
 RUN opam update
-RUN opam install coq.8.20.1 vscoq-language-server
-RUN opam install coq-iris coq-iris-heap-lang coq-iris-unstable
+RUN opam install rocq-core vsrocq-language-server
+RUN opam install rocq-iris rocq-iris-heap-lang rocq-iris-unstable
 
 RUN opam switch stable
 RUN eval $(opam env)
diff --git a/exercises/array_lock.v b/exercises/array_lock.v
index 59ce617..2fc113f 100644
--- a/exercises/array_lock.v
+++ b/exercises/array_lock.v
@@ -167,7 +167,7 @@ Proof.
   iApply inv_alloc.
   iNext.
   iExists 0, 0, _.
-  rewrite (right_id ε (⋅)).
+  rewrite (right_id _ _).
   iFrame "Ha Hn Hγ Hι".
   iLeft.
   iFrame.
@@ -194,7 +194,7 @@ Proof.
   - destruct (decide (o = t)) as [->|H].
     + iPoseProof (lookup_array _ _ _ (t `mod` cap) #true with "Ha") as "[Ht Ha]".
       {
-        apply list_lookup_insert.
+        apply list_lookup_insert_eq.
         rewrite length_replicate.
         apply Nat.mod_upper_bound.
         by apply Nat.lt_neq in Hcap.
@@ -366,7 +366,7 @@ Proof.
   iMod (own_update _ _ (● (Excl' o, GSet (set_seq o (S i))) ⋅ ◯ (None, GSet {[o + i]})) with "Hγ") as "[Hγ Hγ']".
   {
     apply auth_update_alloc, prod_local_update_2.
-    rewrite -(right_id ε (⋅) (GSet {[_]})).
+    rewrite -(right_id _ _ (GSet {[_]})).
     rewrite set_seq_S_end_union_L -gset_disj_union.
     - apply op_local_update_discrete.
       intros _.
@@ -423,7 +423,7 @@ Proof.
   subst o'.
   iPoseProof (update_array _ _ _ (o `mod` cap) #true with "Ha") as "[Ht Ha]".
   {
-    apply list_lookup_insert.
+    apply list_lookup_insert_eq.
     rewrite length_replicate.
     apply Nat.mod_upper_bound.
     by apply Nat.lt_neq in Hcap.
@@ -434,11 +434,14 @@ Proof.
   iSplitL "Hn Hι Hγ Hr Ha Hγ''".
   {
     iNext.
-    rewrite list_insert_insert insert_replicate.
+    rewrite list_insert_insert.
     iExists o, i, _.
     iFrame "Hn Ha Hι Hγ".
     iRight; iLeft.
-    by iFrame.
+    iFrame.
+    iPureIntro.
+    rewrite decide_True //.
+    apply insert_replicate.
   }
   clear i.
   wp_pures.
diff --git a/exercises/custom_ra.v b/exercises/custom_ra.v
index 442aa68..a822b9d 100644
--- a/exercises/custom_ra.v
+++ b/exercises/custom_ra.v
@@ -62,7 +62,7 @@ Global Instance state_equiv_equivalence : Equivalence (≡@{state}) := _.
   To help convert between equivalence and equality, we can tell Iris
   that they coincide, which in this case is trivial.
 *)
-Global Instance state_leibniz_equiv : LeibnizEquiv state := _.
+Global Instance state_leibniz_equiv : LeibnizEquiv state. Proof. by intros ? ?. Qed.
 
 (**
   Recall that resource algebras are discrete cameras and that cameras
diff --git a/exercises/gr_predicates.v b/exercises/gr_predicates.v
index f755011..333ce03 100644
--- a/exercises/gr_predicates.v
+++ b/exercises/gr_predicates.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export fixpoint.
+From iris.bi.lib Require Export fixpoint_mono.
 From iris.heap_lang Require Import lang proofmode notation.
 
 (* ################################################################# *)
diff --git a/exercises/ofe.v b/exercises/ofe.v
index 58cb39c..086e979 100644
--- a/exercises/ofe.v
+++ b/exercises/ofe.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export ofe.
+From iris.algebra Require Export ofe stepindex_finite.
 
 (* ################################################################# *)
 (** * Ordered Families of Equivalences (OFE) *)
@@ -80,7 +80,7 @@ Local Instance stream_dist_instance : Dist stream := λ n s1 s2,
   - [equiv_dist : ∀ x y, x ≡ y ↔ (∀ n, x ≡{n}≡ y)]
     This states that, as the `precision' of the approximation approaches
     infinity, the equivalences approach true equivalence.
-  - [dist_lt : ∀ n m x y, x ≡{n}≡ y → m < n → x ≡{m}≡ y]
+  - [dist_le : ∀ n m x y, x ≡{n}≡ y → m ≤ n → x ≡{m}≡ y]
     This means that reducing the precision can only make more things
     approximately equivalent.
 *)
@@ -110,6 +110,7 @@ End ofe.
 *)
 Global Program Instance stream_cofe : Cofe streamO := {|
   compl c := fun2stream (λ i, nth (c i) i);
+  lbcompl n Hn c := match SIdx.limit_finite n Hn with end;
 |}.
 Next Obligation.
   intros n [c Hc] i Hi; simpl.
@@ -118,6 +119,12 @@ Next Obligation.
   symmetry.
   by apply Hc.
 Qed.
+Next Obligation.
+  intros n Hn. destruct (SIdx.limit_finite n Hn).
+Qed.
+Next Obligation.
+  intros n Hn. destruct (SIdx.limit_finite n Hn).
+Qed.
 
 (**
   There are two important classes of functions between OFEs called
@@ -189,7 +196,8 @@ Proof.
   constructor.
   intros m Hm i Hi.
   apply (H (S i)).
-  lia.
+  transitivity (S m); [lia|].
+  by apply Hm.
 Qed.
 
 
diff --git a/exercises/resource_algebra.v b/exercises/resource_algebra.v
index e272205..c0d2e33 100644
--- a/exercises/resource_algebra.v
+++ b/exercises/resource_algebra.v
@@ -587,7 +587,7 @@ Context {A : ofe}.
 (**
   The carrier of the exclusive RA, [excl], is the same as the carrier of
   the underlying resource algebra with the addition of a bottom element,
-  denoted [ExclBot].
+  denoted [ExclInvalid].
 *)
 
 Print excl.
@@ -600,33 +600,33 @@ Lemma excl_core (ea : excl A) : pcore ea ≡ None.
 Proof. constructor. Qed.
 
 (**
-  Crucially, all elements except [ExclBot] are valid.
+  Crucially, all elements except [ExclInvalid] are valid.
 *)
 
 Lemma excl_valid (a : A) : ✓ (Excl a).
 Proof. constructor. Qed.
 
-Lemma excl_bot_invalid : ¬ (✓ (ExclBot : excl A)).
+Lemma excl_bot_invalid : ¬ (✓ (ExclInvalid : excl A)).
 Proof.
   intros contra.
   inversion contra.
 Qed.
 
 (**
-  And the combination of any two elements gives the invalid [ExclBot].
+  And the combination of any two elements gives the invalid [ExclInvalid].
 *)
 
-Lemma excl_op (ea eb : excl A) : ea ⋅ eb ≡ ExclBot.
+Lemma excl_op (ea eb : excl A) : ea ⋅ eb ≡ ExclInvalid.
 Proof. constructor. Qed.
 
 (**
   Let us return to our beloved dfrac. While the operation for dfrac adds
   two dfrac fractions together, the operation for two _exclusive_ dfrac
-  fractions simply results in [ExclBot].
+  fractions simply results in [ExclInvalid].
 *)
 
 Example excl_op_dfrac :
-  (Excl (DfracOwn (1/4))) ⋅ (Excl (DfracOwn (2/4))) ≡ ExclBot.
+  (Excl (DfracOwn (1/4))) ⋅ (Excl (DfracOwn (2/4))) ≡ ExclInvalid.
 Proof. constructor. Qed.
 
 End exclusive.
@@ -651,7 +651,7 @@ Lemma token_valid : ✓ tok.
 Proof. apply excl_valid. Qed.
 
 (** ... but having the token twice gives the bottom element... *)
-Lemma token_token_bot : tok ⋅ tok ≡ ExclBot.
+Lemma token_token_bot : tok ⋅ tok ≡ ExclInvalid.
 Proof. apply excl_op. Qed.
 
 (* ... which is invalid. *)
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000..fdfbda4
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,27 @@
+{
+  "nodes": {
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1784497964,
+        "narHash": "sha256-vlHUuqAcbcH2RKmHbPiuQzbv1pnzzavXnI62RD0bqCU=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "241313f4e8e508cb9b13278c2b0fa25b9ca27163",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "nixpkgs": "nixpkgs"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..4b12397
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,50 @@
+{
+  description = "Iris tutorial development environment";
+
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
+  };
+
+  outputs =
+    { self, nixpkgs }:
+    let
+      system = "x86_64-linux";
+      pkgs = import nixpkgs { inherit system; };
+    in
+    {
+      devShells.${system}.default = pkgs.mkShell {
+        buildInputs = with pkgs; [
+          rocq-core
+          rocqPackages.stdlib
+          rocqPackages.stdpp
+          rocqPackages.iris
+          rocqPackages.vsrocq-language-server
+          gawk
+          git
+        ];
+      };
+
+      checks.${system}.default = pkgs.stdenv.mkDerivation {
+        name = "iris-tutorial-check";
+        src = ./.;
+        nativeBuildInputs = with pkgs; [
+          rocq-core
+          rocqPackages.stdlib
+          rocqPackages.stdpp
+          rocqPackages.iris
+          gawk
+          git
+        ];
+        buildPhase = ''
+          make -j$NIX_BUILD_CORES all
+          make exercises
+          make html
+        '';
+        installPhase = ''
+          mkdir -p $out/share/doc
+          cp -r html $out/share/doc/html
+          touch $out/done
+        '';
+      };
+    };
+}
diff --git a/iris-tutorial.opam b/iris-tutorial.opam
index 4b892aa..51539a5 100644
--- a/iris-tutorial.opam
+++ b/iris-tutorial.opam
@@ -1,5 +1,5 @@
 opam-version: "2.0"
-name: "coq-iris-tutorial"
+name: "rocq-iris-tutorial"
 synopsis: "A tutorial for the Iris framework"
 maintainer: "The Iris Tutorial Team"
 authors: "The Iris Tutorial Team"
@@ -10,7 +10,7 @@ bug-reports: "https://github.com/logsem/iris-tutorial/issues"
 build: [make "-j%{jobs}%"]
 install: []
 depends: [
-  "coq" { (= "8.20.1") }
-  "coq-iris" { (= "4.3.0") }
-  "coq-iris-heap-lang" { (= "4.3.0") }
+  "rocq-core" { (>= "9.1.0") }
+  "rocq-iris" { (>= "4.5.0") }
+  "rocq-iris-heap-lang" { (>= "4.5.0") }
 ]
diff --git a/theories/array_lock.v b/theories/array_lock.v
index 59ce617..2fc113f 100644
--- a/theories/array_lock.v
+++ b/theories/array_lock.v
@@ -167,7 +167,7 @@ Proof.
   iApply inv_alloc.
   iNext.
   iExists 0, 0, _.
-  rewrite (right_id ε (⋅)).
+  rewrite (right_id _ _).
   iFrame "Ha Hn Hγ Hι".
   iLeft.
   iFrame.
@@ -194,7 +194,7 @@ Proof.
   - destruct (decide (o = t)) as [->|H].
     + iPoseProof (lookup_array _ _ _ (t `mod` cap) #true with "Ha") as "[Ht Ha]".
       {
-        apply list_lookup_insert.
+        apply list_lookup_insert_eq.
         rewrite length_replicate.
         apply Nat.mod_upper_bound.
         by apply Nat.lt_neq in Hcap.
@@ -366,7 +366,7 @@ Proof.
   iMod (own_update _ _ (● (Excl' o, GSet (set_seq o (S i))) ⋅ ◯ (None, GSet {[o + i]})) with "Hγ") as "[Hγ Hγ']".
   {
     apply auth_update_alloc, prod_local_update_2.
-    rewrite -(right_id ε (⋅) (GSet {[_]})).
+    rewrite -(right_id _ _ (GSet {[_]})).
     rewrite set_seq_S_end_union_L -gset_disj_union.
     - apply op_local_update_discrete.
       intros _.
@@ -423,7 +423,7 @@ Proof.
   subst o'.
   iPoseProof (update_array _ _ _ (o `mod` cap) #true with "Ha") as "[Ht Ha]".
   {
-    apply list_lookup_insert.
+    apply list_lookup_insert_eq.
     rewrite length_replicate.
     apply Nat.mod_upper_bound.
     by apply Nat.lt_neq in Hcap.
@@ -434,11 +434,14 @@ Proof.
   iSplitL "Hn Hι Hγ Hr Ha Hγ''".
   {
     iNext.
-    rewrite list_insert_insert insert_replicate.
+    rewrite list_insert_insert.
     iExists o, i, _.
     iFrame "Hn Ha Hι Hγ".
     iRight; iLeft.
-    by iFrame.
+    iFrame.
+    iPureIntro.
+    rewrite decide_True //.
+    apply insert_replicate.
   }
   clear i.
   wp_pures.
diff --git a/theories/custom_ra.v b/theories/custom_ra.v
index 9862cea..1e89f9f 100644
--- a/theories/custom_ra.v
+++ b/theories/custom_ra.v
@@ -62,7 +62,7 @@ Global Instance state_equiv_equivalence : Equivalence (≡@{state}) := _.
   To help convert between equivalence and equality, we can tell Iris
   that they coincide, which in this case is trivial.
 *)
-Global Instance state_leibniz_equiv : LeibnizEquiv state := _.
+Global Instance state_leibniz_equiv : LeibnizEquiv state. Proof. by intros ? ?. Qed.
 
 (**
   Recall that resource algebras are discrete cameras and that cameras
@@ -271,7 +271,7 @@ Lemma thread_spec γ l (x : Z) : {{{inv N (state_inv γ l x)}}} #l <- !#l + #1 {
   { iExists y. iFrame. }
   wp_pures.
   iInv N as ">(%z & Hl & H)".
-  iAssert (∃ s, own γ s)%I with "[H]" as (s) "Hγ".
+  iAssert (∃ s : state, own γ s)%I with "[H]" as (s) "Hγ".
   {
     iDestruct "H" as "[[Hγ _]|[Hγ _]]".
     - by iExists Start.
diff --git a/theories/gr_predicates.v b/theories/gr_predicates.v
index f755011..333ce03 100644
--- a/theories/gr_predicates.v
+++ b/theories/gr_predicates.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export fixpoint.
+From iris.bi.lib Require Export fixpoint_mono.
 From iris.heap_lang Require Import lang proofmode notation.
 
 (* ################################################################# *)
diff --git a/theories/ofe.v b/theories/ofe.v
index 1abbb96..b7e91f5 100644
--- a/theories/ofe.v
+++ b/theories/ofe.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export ofe.
+From iris.algebra Require Export ofe stepindex_finite.
 
 (* ################################################################# *)
 (** * Ordered Families of Equivalences (OFE) *)
@@ -82,7 +82,7 @@ Local Instance stream_dist_instance : Dist stream := λ n s1 s2,
   - [equiv_dist : ∀ x y, x ≡ y ↔ (∀ n, x ≡{n}≡ y)]
     This states that, as the `precision' of the approximation approaches
     infinity, the equivalences approach true equivalence.
-  - [dist_lt : ∀ n m x y, x ≡{n}≡ y → m < n → x ≡{m}≡ y]
+  - [dist_le : ∀ n m x y, x ≡{n}≡ y → m ≤ n → x ≡{m}≡ y]
     This means that reducing the precision can only make more things
     approximately equivalent.
 *)
@@ -109,7 +109,7 @@ Proof.
       * by apply H2.
   - intros n m s1 s2 H Hm i Hi.
     apply H.
-    lia.
+    transitivity m; done.
 Qed.
 (* END SOLUTION BEGIN TEMPLATE
   (* exercise *)
@@ -136,6 +136,7 @@ End ofe.
 *)
 Global Program Instance stream_cofe : Cofe streamO := {|
   compl c := fun2stream (λ i, nth (c i) i);
+  lbcompl n Hn c := match SIdx.limit_finite n Hn with end;
 |}.
 Next Obligation.
   intros n [c Hc] i Hi; simpl.
@@ -144,6 +145,12 @@ Next Obligation.
   symmetry.
   by apply Hc.
 Qed.
+Next Obligation.
+  intros n Hn. destruct (SIdx.limit_finite n Hn).
+Qed.
+Next Obligation.
+  intros n Hn. destruct (SIdx.limit_finite n Hn).
+Qed.
 
 (**
   There are two important classes of functions between OFEs called
@@ -215,7 +222,8 @@ Proof.
   constructor.
   intros m Hm i Hi.
   apply (H (S i)).
-  lia.
+  transitivity (S m); [lia|].
+  by apply Hm.
 Qed.
 
 
diff --git a/theories/resource_algebra.v b/theories/resource_algebra.v
index c250030..918b346 100644
--- a/theories/resource_algebra.v
+++ b/theories/resource_algebra.v
@@ -604,7 +604,7 @@ Context {A : ofe}.
 (**
   The carrier of the exclusive RA, [excl], is the same as the carrier of
   the underlying resource algebra with the addition of a bottom element,
-  denoted [ExclBot].
+  denoted [ExclInvalid].
 *)
 
 Print excl.
@@ -617,33 +617,33 @@ Lemma excl_core (ea : excl A) : pcore ea ≡ None.
 Proof. constructor. Qed.
 
 (**
-  Crucially, all elements except [ExclBot] are valid.
+  Crucially, all elements except [ExclInvalid] are valid.
 *)
 
 Lemma excl_valid (a : A) : ✓ (Excl a).
 Proof. constructor. Qed.
 
-Lemma excl_bot_invalid : ¬ (✓ (ExclBot : excl A)).
+Lemma excl_bot_invalid : ¬ (✓ (ExclInvalid : excl A)).
 Proof.
   intros contra.
   inversion contra.
 Qed.
 
 (**
-  And the combination of any two elements gives the invalid [ExclBot].
+  And the combination of any two elements gives the invalid [ExclInvalid].
 *)
 
-Lemma excl_op (ea eb : excl A) : ea ⋅ eb ≡ ExclBot.
+Lemma excl_op (ea eb : excl A) : ea ⋅ eb ≡ ExclInvalid.
 Proof. constructor. Qed.
 
 (**
   Let us return to our beloved dfrac. While the operation for dfrac adds
   two dfrac fractions together, the operation for two _exclusive_ dfrac
-  fractions simply results in [ExclBot].
+  fractions simply results in [ExclInvalid].
 *)
 
 Example excl_op_dfrac :
-  (Excl (DfracOwn (1/4))) ⋅ (Excl (DfracOwn (2/4))) ≡ ExclBot.
+  (Excl (DfracOwn (1/4))) ⋅ (Excl (DfracOwn (2/4))) ≡ ExclInvalid.
 Proof. constructor. Qed.
 
 End exclusive.
@@ -668,7 +668,7 @@ Lemma token_valid : ✓ tok.
 Proof. apply excl_valid. Qed.
 
 (** ... but having the token twice gives the bottom element... *)
-Lemma token_token_bot : tok ⋅ tok ≡ ExclBot.
+Lemma token_token_bot : tok ⋅ tok ≡ ExclInvalid.
 Proof. apply excl_op. Qed.
 
 (* ... which is invalid. *)

From 1f86179f259f3e583e974f9137c51e3167d23bc7 Mon Sep 17 00:00:00 2001
From: Serhii Khoma <sergey@nordicresults.com>
Date: Wed, 22 Jul 2026 21:34:27 +0700
Subject: [PATCH 2/8] feat: update to latest rocq -> sed /coq/rocq/

---
 .devcontainer/arm64/devcontainer.json         |  2 +-
 .devcontainer/x86-64/devcontainer.json        |  2 +-
 .gitignore                                    | 16 +++----
 Makefile                                      | 24 +++++-----
 README.md                                     | 45 ++++++++++++++----
 TODO.md                                       |  7 ++-
 _CoqProject => _RocqProject                   |  0
 coqdocjs/README.md                            | 44 ------------------
 coqdocjs/example/.gitignore                   |  3 --
 coqdocjs/example/Makefile                     | 21 ---------
 coqdocjs/example/README.md                    |  4 --
 coqdocjs/extra/footer.html                    |  8 ----
 coqdocjs/extra/header.html                    | 26 -----------
 docker_image/Dockerfile                       |  2 +-
 exercises/basics.v                            | 36 +++++++--------
 exercises/custom_ra.v                         |  2 +-
 exercises/gr_predicates.v                     | 11 +++--
 exercises/lang.v                              |  6 +--
 exercises/ofe.v                               |  2 +-
 exercises/pure.v                              | 20 ++++----
 exercises/resource_algebra.v                  | 10 ++--
 exercises/specifications.v                    |  4 +-
 flake.nix                                     |  4 +-
 {coqdocjs => rocqdocjs}/.gitignore            |  2 +-
 {coqdocjs => rocqdocjs}/LICENSE               |  0
 {coqdocjs => rocqdocjs}/Makefile.doc          | 18 ++++----
 rocqdocjs/README.md                           | 46 +++++++++++++++++++
 rocqdocjs/example/.gitignore                  |  3 ++
 rocqdocjs/example/Makefile                    | 21 +++++++++
 .../example/Makefile.coq.local                |  0
 rocqdocjs/example/README.md                   |  5 ++
 {coqdocjs => rocqdocjs}/example/_CoqProject   |  0
 {coqdocjs => rocqdocjs}/example/a.v           |  0
 .../example/coqdocjs/Makefile.doc             |  0
 .../example/coqdocjs/extra                    |  0
 rocqdocjs/extra/footer.html                   |  9 ++++
 rocqdocjs/extra/header.html                   | 28 +++++++++++
 .../extra/resources/config.js                 |  8 ++--
 .../extra/resources/coqdoc.css                |  0
 .../extra/resources/coqdocjs.css              |  0
 .../extra/resources/coqdocjs.js               | 14 +++---
 theories/basics.v                             | 36 +++++++--------
 theories/custom_ra.v                          |  2 +-
 theories/gr_predicates.v                      | 11 +++--
 theories/lang.v                               |  6 +--
 theories/ofe.v                                |  2 +-
 theories/pure.v                               | 20 ++++----
 theories/resource_algebra.v                   | 10 ++--
 theories/specifications.v                     |  4 +-
 49 files changed, 291 insertions(+), 253 deletions(-)
 rename _CoqProject => _RocqProject (100%)
 delete mode 100644 coqdocjs/README.md
 delete mode 100644 coqdocjs/example/.gitignore
 delete mode 100644 coqdocjs/example/Makefile
 delete mode 100644 coqdocjs/example/README.md
 delete mode 100644 coqdocjs/extra/footer.html
 delete mode 100644 coqdocjs/extra/header.html
 rename {coqdocjs => rocqdocjs}/.gitignore (95%)
 rename {coqdocjs => rocqdocjs}/LICENSE (100%)
 rename {coqdocjs => rocqdocjs}/Makefile.doc (56%)
 create mode 100644 rocqdocjs/README.md
 create mode 100644 rocqdocjs/example/.gitignore
 create mode 100644 rocqdocjs/example/Makefile
 rename {coqdocjs => rocqdocjs}/example/Makefile.coq.local (100%)
 create mode 100644 rocqdocjs/example/README.md
 rename {coqdocjs => rocqdocjs}/example/_CoqProject (100%)
 rename {coqdocjs => rocqdocjs}/example/a.v (100%)
 rename {coqdocjs => rocqdocjs}/example/coqdocjs/Makefile.doc (100%)
 rename {coqdocjs => rocqdocjs}/example/coqdocjs/extra (100%)
 create mode 100644 rocqdocjs/extra/footer.html
 create mode 100644 rocqdocjs/extra/header.html
 rename {coqdocjs => rocqdocjs}/extra/resources/config.js (89%)
 rename {coqdocjs => rocqdocjs}/extra/resources/coqdoc.css (100%)
 rename {coqdocjs => rocqdocjs}/extra/resources/coqdocjs.css (100%)
 rename {coqdocjs => rocqdocjs}/extra/resources/coqdocjs.js (95%)

diff --git a/.devcontainer/arm64/devcontainer.json b/.devcontainer/arm64/devcontainer.json
index 34ed0be..92483f5 100644
--- a/.devcontainer/arm64/devcontainer.json
+++ b/.devcontainer/arm64/devcontainer.json
@@ -3,7 +3,7 @@
 	"image": "ghcr.io/logsem/iris-tutorial/docker-arm64",
 	"customizations": {
 		"vscode": {
-		  "extensions": ["maximedenes.vscoq"]
+		  "extensions": ["maximedenes.vsrocq"]
 		},
 		"settings": {
 			"terminal.integrated.profiles.linux": {
diff --git a/.devcontainer/x86-64/devcontainer.json b/.devcontainer/x86-64/devcontainer.json
index eee7e6e..68b8322 100644
--- a/.devcontainer/x86-64/devcontainer.json
+++ b/.devcontainer/x86-64/devcontainer.json
@@ -3,7 +3,7 @@
 	"image": "ghcr.io/logsem/iris-tutorial/docker-x86-64",
 	"customizations": {
 		"vscode": {
-		  "extensions": ["maximedenes.vscoq"]
+		  "extensions": ["maximedenes.vsrocq"]
 		},
 		"settings": {
 			"terminal.integrated.profiles.linux": {
diff --git a/.gitignore b/.gitignore
index 45b5766..4108a1a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,7 +3,7 @@
 *.vok
 *.vio
 *.v.d
-.coqdeps.d
+.rocqdeps.d
 *.glob
 *.cache
 *.aux
@@ -11,15 +11,15 @@
 .\#*
 *~
 *.bak
-.coqdeps.d
-.coq-native/
-*.crashcoqide
+.rocqdeps.d
+.rocq-native/
+*.crashrocqide
 .env
 builddep/
-_CoqProject.*
-Makefile.coq
-Makefile.coq.conf
-.Makefile.coq.d
+_RocqProject.*
+Makefile.rocq
+Makefile.rocq.conf
+.Makefile.rocq.d
 Makefile.package.*
 .Makefile.package.*
 _opam
diff --git a/Makefile b/Makefile
index f80f881..06ade92 100644
--- a/Makefile
+++ b/Makefile
@@ -1,30 +1,30 @@
 SOLUTIONS := $(wildcard theories/*.v)
 EXERCISES := $(addprefix exercises/,$(notdir $(SOLUTIONS)))
 
-EXTRA_DIR:=coqdocjs/extra
-COQDOCFLAGS:= \
+EXTRA_DIR:=rocqdocjs/extra
+ROCQDOCFLAGS:= \
   --toc --toc-depth 2 --html --interpolate \
   --index indexpage --no-lib-name --parse-comments \
   --with-header $(EXTRA_DIR)/header.html --with-footer $(EXTRA_DIR)/footer.html
-export COQDOCFLAGS
+export ROCQDOCFLAGS
 
-all: Makefile.coq
-	+make -f Makefile.coq all
+all: Makefile.rocq
+	+make -f Makefile.rocq all
 .PHONY: all
 
-clean: Makefile.coq
-	+make -f Makefile.coq clean
-	rm -f Makefile.coq
+clean: Makefile.rocq
+	+make -f Makefile.rocq clean
+	rm -f Makefile.rocq
 .PHONY: clean
 
-html: Makefile.coq _CoqProject
+html: Makefile.rocq _RocqProject
 	rm -fr html
-	+make -f Makefile.coq $@
+	+make -f Makefile.rocq $@
 	cp -R $(EXTRA_DIR)/resources html
 .PHONY: html
 
-Makefile.coq: _CoqProject
-	rocq makefile -f _CoqProject -o Makefile.coq
+Makefile.rocq: _RocqProject
+	rocq makefile -f _RocqProject -o Makefile.rocq
 
 exercises: $(EXERCISES)
 .PHONY: exercises
diff --git a/README.md b/README.md
index f7dfef8..aa8936d 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,5 @@
 # Iris Tutorial
+
 The Iris Tutorial is an introduction to the [Iris separation logic framework](https://iris-project.org/) and how to work with its [Rocq formalization](https://gitlab.mpi-sws.org/iris/iris/).
 
 The exposition is intended for a broad range of readers from advanced undergraduates to PhD students and researchers. We assume that readers are already motivated to learn Iris and thus present the material in a bottom-up fashion, rather than starting out with cool motivating examples. The tutorial material is intended to be self-contained. No specific background in logic or programming languages is assumed but some familiarity with basic programming languages theory and discrete mathematics will be beneficial, see e.g. [TAPL](https://www.cis.upenn.edu/~bcpierce/tapl/). Additionally, basic knowledge of the Rocq prover is assumed. Advanced Rocq tactics have been purposefully kept to a minimum, and some proofs are longer than necessary to facilitate learning. We demonstrate more advanced tactics in chapter [ticket_lock_advanced](/theories/ticket_lock_advanced.v).
@@ -11,34 +12,42 @@ The tutorial comes in two versions:
 The tutorial consists of several chapters, each corresponding to a Rocq file. The graph in [Chapter Dependencies](README.md#chapter-dependencies) illustrates possible ways to go through the tutorial. However, the recommended order is specified in the [Recommended Learning Path](README.md#recommended-learning-path).
 
 ## Setup
+
 This version is known to compile with
 
-- Rocq 8.20.1
-- Iris 4.3.0
+- Rocq 9.1.1
+- Iris 4.5.0
 
 The recommended way to install the dependencies is through [opam](https://opam.ocaml.org/doc/Install.html).
 
 1. Install [opam](https://opam.ocaml.org/doc/Install.html) if not already installed (a version greater than 2.0 is required).
 2. Install a new switch and link it to the project. From the root of the repository, execute
-```
+
+```sh
 opam switch create iris_tutorial 5.2.0
 opam switch link iris_tutorial .
 ```
+
 3. Add the Rocq opam repository.
-```
-opam repo add coq-released https://coq.inria.fr/opam/released
+
+```sh
+opam repo add rocq-released https://rocq-prover.org/opam/released
 opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
 opam update
 ```
+
 4. Install the right version of the dependencies as specified in the `iris-tutorial.opam` file.
-```
+
+```sh
 opam install . --deps-only
 ```
 
 ## Editor
+
 Iris makes extensive use of Unicode characters. [This guide](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/editor.md) describes how to set up your favorite editor.
 
 ## Chapter Overview
+
 - [basics](/exercises/basics.v) - Introduction to the separation
   logic and the Iris Proof Mode
 - [pure](/exercises/pure.v) - Distinction between the Rocq context and the Iris context
@@ -64,6 +73,7 @@ Iris makes extensive use of Unicode characters. [This guide](https://gitlab.mpi-
 - [ofe](/exercises/ofe.v) - Detailed introduction to OFEs
 
 ## Chapter Dependencies
+
 ```mermaid
 graph TD;
   basics --> pure;
@@ -104,6 +114,7 @@ graph TD;
 ```
 
 ## Recommended Learning Path
+
 To get a good understanding of the fundamental concepts of Iris, it is recommended to study the following chapters in the given order.
 
 1. [basics](/exercises/basics.v)
@@ -124,6 +135,7 @@ To get a good understanding of the fundamental concepts of Iris, it is recommend
 16. [adequacy](/exercises/adequacy.v)
 
 ## Exercises
+
 To work on the exercises, simply edit the files in the `exercises/` folder. Some proofs and definitions are admitted and marked as `(* exercise *)`---your task is to fill in those definitions and complete the proofs all the way to `Qed`.
 
 After you are done with a file, run `make` (with your working directory being the repository root, where the `Makefile` is located) to compile and check the exercises.
@@ -131,6 +143,7 @@ After you are done with a file, run `make` (with your working directory being th
 If you are stuck, you can find solutions in the corresponding file in the `theories/` folder.
 
 ## Documentation
+
 This [cheatsheet](/cheatsheet.md) contains a table of the most important tactics for each logical connective. A full description of the Iris Proof Mode tactics can be found in the files [proof_mode.md](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/proof_mode.md) and [heap_lang.md](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/heap_lang.md).
 
 ## Optional Reading
@@ -160,42 +173,55 @@ To contribute, we recommend following these steps:
 For more detailed instructions, see [first-contributions](
 https://github.com/firstcontributions/first-contributions).
 
-### CoqdocJS
-This tutorial uses [CoqdocJS](https://github.com/coq-community/coqdocjs), so please make sure to format your changes accordingly. To see what your changes will look like in the documentation, run
-```
+### RocqdocJS
+
+This tutorial uses [RocqdocJS](https://github.com/rocq-community/rocqdocjs), so please make sure to format your changes accordingly. To see what your changes will look like in the documentation, run
+
+```sh
 git submodule update --init
 make html
 ```
+
 Then open `html/toc.html` in a browser, and navigate to the chapter(s) containing your changes.
 
 ### Generating the Exercises
+
 Note that the files in `exercises/` are generated from the corresponding files in `theories/`. As such, if you wish to make changes to a chapter, please make those changes to the `theories`-version of the chapter. Afterwards, the `exercises`-version can be re-generated by running `make exercises`. This requires `gawk` to be installed (which should be available on Linux, and on macOS can be installed via `brew install gawk`).
 
 The syntax for the solution files is as follows:
 
+```rocq
     (* SOLUTION *) Proof.
       solution here.
     Qed.
+```
 
 is replaced by
 
+```rocq
     Proof.
       (* exercise *)
     Admitted.
+```
 
 and the more powerful
 
+```rocq
     (* BEGIN SOLUTION *)
       solution here.
     (* END SOLUTION BEGIN TEMPLATE
       exercise template here.
     END TEMPLATE *)
+```
 
 is replaced by
 
+```rocq
       exercise template here.
+```
 
 ### Contact
+
 If you have specific requests or questions about the tutorial, please contact:
 
 **Amin Timany**\
@@ -203,6 +229,7 @@ Aarhus University\
 <timany@cs.au.dk>
 
 ### Contributors
+
 Below is a list of people who have contributed to the tutorial, sorted by last name. If you have contributed to the project, please add yourself to the list.
 
 **Lars Birkedal**\
diff --git a/TODO.md b/TODO.md
index 498e444..ec8afe6 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,10 +1,12 @@
 # Fixes
+
 - The chapter [gr_predicates.v] does actually not talk about guarded fixpoints, only least fixpoints
 - Clean up proofs in some chapters
   - Reduce use of SSreflect
   - Simplify proofs
 
 # Possible future topics
+
 - Chapter on prophecies
 - Chapter on HOCAP-style specifications
 - Chapters "Linked List", "Arrays", and "Merge Sort" all use list functionality from std++ (e.g. fmap and lookup). These should be introduced beforehand, for example in an appendix, with the chapters referring to the appendix.
@@ -24,5 +26,6 @@
 - How to define logical relations models of type systems in Iris.
 
 # Features
-- Make tutorial accessible as an interactive webpage (jscoq)
-  - See e.g. https://jscoq.github.io/ext/sf/
+
+- Make tutorial accessible as an interactive webpage (jsrocq)
+  - See e.g. <https://jsrocq.github.io/ext/sf/>
diff --git a/_CoqProject b/_RocqProject
similarity index 100%
rename from _CoqProject
rename to _RocqProject
diff --git a/coqdocjs/README.md b/coqdocjs/README.md
deleted file mode 100644
index 685d4a3..0000000
--- a/coqdocjs/README.md
+++ /dev/null
@@ -1,44 +0,0 @@
-# CoqdocJS
-
-CoqdocJS is a little script to dynamically improve the coqdoc output.
-The result can be seen here:
-
-https://www.ps.uni-saarland.de/autosubst/doc/Ssr.POPLmark.html
-
-It offers the following features:
-- Customizable Unicode display:
-	It only changes the display, copy-paste from the website produces pure ASCII.
-	It only replaces complete identifiers or notation tokens, possibly terminated by numbers or apostrophes.
-	It does not replace randomly, like in "omega." or "tauto."
-	To add new symbols, edit [config.js](extra/resources/config.js).
-- Proof hiding:
-	All proofs longer than one line are hidden by default. They can be uncovered by clicking on "Proof...".
-
-All of this works with the ordinary coqdoc, by asking coqdoc to use a header file including the javascript files and some custom CSS.
-
-## Usage
-
-1. Clone this repository as a subdirectory or submodule;
-2. Include [Makefile.doc] in your `Makefile`, or copy it as, e.g., `Makefile.coq.local`;
-3. Run `make coqdoc` to build documentations.
-
-A minimal example is shown [here](example).
-
-### Environment Variables
-Name | Usage | Default
----|---|---
-`COQDOCFLAGS` | Override the flags passed to `coqdoc` | see [Makefile.doc]
-`COQDOCEXTRAFLAGS` | Extend the flags passed to `coqdoc` | empty
-`COQDOCJS_LN` | If set to `true` then symlink resource files; otherwise copy | `false`
-`COQDOCJS_DIR` | Folder containing CoqdocJS | `coqdocjs`
-`COQMAKEFILE` | Makefile generated by `coq_makefile` | `Makefile.coq`
-
-## Files
-
-- [Makefile.doc]: a generic Makefile setup that calls coqc and coqdoc with the right parameters
-- [config.js](extra/resources/config.js): contains the unicode replacement table
-- [coqdoc.css](extra/resources/coqdoc.css): a replacement for the default Coqdoc CSS style. Can be removed to use the default style
-- [coqdocjs.js](extra/resources/coqdocjs.js) and [coqdocjs.css](extra/resources/coqdocjs.css): the script rewriting the DOM and adding the dynamic features with a corresponding CSS style
-- [header.html](extra/header.html) and [footer.html](extra/footer.html): custom header and footer files used in every generated html file
-
-[Makefile.doc]: Makefile.doc
diff --git a/coqdocjs/example/.gitignore b/coqdocjs/example/.gitignore
deleted file mode 100644
index a3200a7..0000000
--- a/coqdocjs/example/.gitignore
+++ /dev/null
@@ -1,3 +0,0 @@
-Makefile.coq
-Makefile.coq.conf
-html/
diff --git a/coqdocjs/example/Makefile b/coqdocjs/example/Makefile
deleted file mode 100644
index 4829da8..0000000
--- a/coqdocjs/example/Makefile
+++ /dev/null
@@ -1,21 +0,0 @@
-COQMAKEFILE ?= Makefile.coq
-COQDOCEXTRAFLAGS = -s
-COQDOCJS_LN = true
-COQ_PROJ ?= _CoqProject
-
-all: $(COQMAKEFILE)
-	$(MAKE) -f $^ $@
-
-clean: $(COQMAKEFILE)
-	$(MAKE) -f $^ cleanall
-	$(RM) $^ $^.conf
-
-$(COQMAKEFILE): $(COQ_PROJ)
-	$(COQBIN)coq_makefile -f $^ -o $@
-
-force $(COQ_PROJ) Makefile: ;
-
-%: $(COQMAKEFILE) force
-	@+$(MAKE) -f $< $@
-
-.PHONY: clean all force
diff --git a/coqdocjs/example/README.md b/coqdocjs/example/README.md
deleted file mode 100644
index 8172989..0000000
--- a/coqdocjs/example/README.md
+++ /dev/null
@@ -1,4 +0,0 @@
-# CoqdocJS Usage Example
-This folder contains a minimal example to use CoqdocJS in your project.
-
-You can build the docs with `make coqdoc`.
diff --git a/coqdocjs/extra/footer.html b/coqdocjs/extra/footer.html
deleted file mode 100644
index 2ff40b3..0000000
--- a/coqdocjs/extra/footer.html
+++ /dev/null
@@ -1,8 +0,0 @@
-</div>
-<div id="footer">
-  Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/coq-community/coqdocjs">CoqdocJS</a>
-</div>
-</div>
-</body>
-
-</html>
diff --git a/coqdocjs/extra/header.html b/coqdocjs/extra/header.html
deleted file mode 100644
index c064d5a..0000000
--- a/coqdocjs/extra/header.html
+++ /dev/null
@@ -1,26 +0,0 @@
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
-<html xmlns="http://www.w3.org/1999/xhtml">
-
-<head>
-<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
-<link href="resources/coqdoc.css" rel="stylesheet" type="text/css" />
-<link href="resources/coqdocjs.css" rel="stylesheet" type="text/css"/>
-<script type="text/javascript" src="resources/config.js"></script>
-<script type="text/javascript" src="resources/coqdocjs.js"></script>
-</head>
-
-<body onload="document.getElementById('content').focus()">
-  <div id="header">
-    <span class="left">
-      <span class="modulename"> <script> document.write(document.title) </script> </span>
-    </span>
-
-    <span class="button" id="toggle-proofs"></span>
-
-    <span class="right">
-      <a href="./indexpage.html"> Index </a>
-      <a href="./toc.html"> Table of Contents </a>
-    </span>
-</div>
-    <div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
-    <div id="main">
diff --git a/docker_image/Dockerfile b/docker_image/Dockerfile
index 646fa45..2c7a6aa 100644
--- a/docker_image/Dockerfile
+++ b/docker_image/Dockerfile
@@ -13,7 +13,7 @@ RUN rm -rf opam
 
 RUN opam init
 RUN eval $(opam env)
-RUN opam repo add --set-default coq-released https://coq.inria.fr/opam/released
+RUN opam repo add --set-default rocq-released https://rocq-prover.org/opam/released
 RUN opam repo add --set-default iris-dev https://gitlab.mpi-sws.org/iris/opam.git
 
 RUN opam switch create stable ocaml.5.2.0
diff --git a/exercises/basics.v b/exercises/basics.v
index e9c564e..5962988 100644
--- a/exercises/basics.v
+++ b/exercises/basics.v
@@ -51,7 +51,7 @@ From iris.proofmode Require Import proofmode.
 *)
 
 (* ================================================================= *)
-(** ** Iris in Coq *)
+(** ** Iris in Rocq *)
 
 (**
   The type of propositions in Iris is [iProp Σ]. All proofs in Iris are
@@ -67,17 +67,17 @@ Section proofs.
 Context {Σ: gFunctors}.
 
 (**
-  Iris defines two Coq propositions for proving Iris propositions:
+  Iris defines two Rocq propositions for proving Iris propositions:
   - [⊢ P] asks whether [P] holds with no assumptions
   - [P ⊢ Q] asks whether [Q] holds assuming [P]
 
-  Iris is built on top of Coq, so to smoothen the experience, we will be
+  Iris is built on top of Rocq, so to smoothen the experience, we will be
   working with the Iris Proof Mode (IPM). The practical implication of
   this is that we get a new context, called the spatial context, in
   addition to the usual context, now called the non-spatial context.
   Hypotheses from both contexts can be used to prove the goal.
 
-  The regular Coq tactics can still be used when we work within the
+  The regular Rocq tactics can still be used when we work within the
   non-spatial context, but, in general, we shall use new tactics that
   work natively with the spatial context. These new tactics start with
   'i', and since many of them simply 'lift' the regular tactics to also
@@ -85,7 +85,7 @@ Context {Σ: gFunctors}.
   the 'i' prefixed. For instance, instead of [intros H] we use
   [iIntros "H"], and instead of [apply H] we use [iApply "H"]. Note that
   identifiers for hypotheses in the spatial context are strings, instead
-  of the usual Coq identifiers.
+  of the usual Rocq identifiers.
 
   To see this in action we will prove the statement [P ⊢ P], for all
   [P].
@@ -111,12 +111,12 @@ Qed.
 (** *** Technical Details *)
 
 (**
-  In Coq, the context and the goal is a sequent (we use [⊢ₓ] for
-  the Coq entailment to distinguish it from the Iris entailment [⊢]):
+  In Rocq, the context and the goal is a sequent (we use [⊢ₓ] for
+  the Rocq entailment to distinguish it from the Iris entailment [⊢]):
 
                     [H₁ : Φ₁, ..., Hₙ : Φₙ ⊢ₓ Ψ]
 
-  Here, the left-hand side of the Coq entailment [⊢ₓ] is the
+  Here, the left-hand side of the Rocq entailment [⊢ₓ] is the
   (non-spatial) context and the right-hand side is the goal. This
   sequent is equivalent to the entailment [Φ₁ ∧ ... ∧ Φₙ ⊢ₓ Ψ].
 
@@ -128,17 +128,17 @@ Qed.
   However, as Iris is a separation logic, this is equivalent to the
   entailment [Φ₁ ∗ ... ∗ Φₙ ⊢ Ψ].
 
-  Technically, since Iris is built on top of Coq, proving an Iris
-  entailment in Coq corresponds to proving [⊢ₓ (P ⊢ Q)]. In other
-  words, the spatial context is part of the Coq goal. This is the reason
-  why the regular Coq tactics no longer suffice. The new tactics work
+  Technically, since Iris is built on top of Rocq, proving an Iris
+  entailment in Rocq corresponds to proving [⊢ₓ (P ⊢ Q)]. In other
+  words, the spatial context is part of the Rocq goal. This is the reason
+  why the regular Rocq tactics no longer suffice. The new tactics work
   with both the non-spatial and the spatial contexts.
 *)
 
 (**
   Iris propositions include many of the usual logical connectives such
   as conjunction [P ∧ Q]. As such, Iris uses a notation scope to
-  overload the usual logical notation in Coq. This scope is delimited by
+  overload the usual logical notation in Rocq. This scope is delimited by
   [I] and bound to [iProp Σ]. Hence, you may need to wrap your
   propositions in [(_)%I] to use the notations.
 *)
@@ -226,8 +226,8 @@ Proof.
 Admitted.
 
 (**
-  Just as with Coq tactics, Iris allows nesting of introduction
-  patterns. In fact, like Coq, Iris supports patterns of the form
+  Just as with Rocq tactics, Iris allows nesting of introduction
+  patterns. In fact, like Rocq, Iris supports patterns of the form
   [(H1 & .. & H2 & H3)] as a shorthand for [[H1 .. [H2 H3] ..]].
 
   Exercise: try to use an introduction with a pattern of parentheses to
@@ -293,7 +293,7 @@ Proof.
 Admitted.
 
 (**
-  Disjunctions [∨] are treated just like disjunctions in Coq. The
+  Disjunctions [∨] are treated just like disjunctions in Rocq. The
   introduction pattern [[ _ | _ ]] allows us to eliminate a disjunction,
   while the tactics [iLeft] and [iRight] let us introduce them.
 
@@ -324,7 +324,7 @@ Proof.
 Admitted.
 
 (**
-  Iris has existential and universal quantifiers over any Coq type.
+  Iris has existential and universal quantifiers over any Rocq type.
   Existential quantifiers are proved using the [iExists] tactic, using
   the same syntax as for [exists]. Elimination of existentials is done
   through the pattern ["[%_ _]"] or as part of a ["(_&..&_)"] with a [%]
@@ -341,7 +341,7 @@ Proof.
 Admitted.
 
 (**
-  Likewise, forall quantification works almost as in Coq. To introduce
+  Likewise, forall quantification works almost as in Rocq. To introduce
   universally quantified variables, you can either use [iIntros (x y z)]
   or [iIntros "%x %y %z"]. These patterns are interchangeable. To
   specify the parameters of hypotheses, we write
diff --git a/exercises/custom_ra.v b/exercises/custom_ra.v
index a822b9d..60979ff 100644
--- a/exercises/custom_ra.v
+++ b/exercises/custom_ra.v
@@ -130,7 +130,7 @@ Qed.
 
 (**
   The final step is to package this into a CMRA structure, allowing us
-  to use the resource algebra in proofs (using Coq's Context mechanism).
+  to use the resource algebra in proofs (using Rocq's Context mechanism).
 *)
 Canonical Structure stateR := discreteR state state_ra_mixin.
 
diff --git a/exercises/gr_predicates.v b/exercises/gr_predicates.v
index 333ce03..b8ee3ce 100644
--- a/exercises/gr_predicates.v
+++ b/exercises/gr_predicates.v
@@ -6,12 +6,12 @@ From iris.heap_lang Require Import lang proofmode notation.
 
 (**
   In the Linked List chapter, we defined a representation predicate for
-  linked lists using Coq's Fixpoint mechanism. In this chapter, we
+  linked lists using Rocq's Fixpoint mechanism. In this chapter, we
   present an alternative approach to defining representation predicates,
   which instead uses fixpoints of predicates. The high-level point to
   notice is that we can define fixpoints of monotone functions on Iris
   predicates, much in the same way as one can define fixpoints of
-  monotone function on Coq predicates. Later on, we will discuss
+  monotone function on Rocq predicates. Later on, we will discuss
   different kinds of fixpoints in more detail.
 *)
 
@@ -20,9 +20,10 @@ Context `{!heapGS Σ}.
 
 (**
   As we have already seen, we can define a predicate for linked lists
-  representing a list of specific values, using Coq's notion of fixpoint
-  for the inductive Coq type [list val].
+  representing a list of specific values, using Rocq's notion of fixpoint
+  for the inductive Rocq type [list val].
 *)
+
 Fixpoint is_list_of (v : val) (xs : list val) : iProp Σ :=
   match xs with
   | [] => ⌜v = NONEV⌝
@@ -33,7 +34,7 @@ Fixpoint is_list_of (v : val) (xs : list val) : iProp Σ :=
   However, sometimes we don't care about the exact list and instead, we
   only want to know that each value of the list satisfies some
   predicate. This can be captured by using a helper predicate [all]
-  expressing that all elements of a Coq list satisfy a predicate.
+  expressing that all elements of a Rocq list satisfy a predicate.
 *)
 Fixpoint all (xs : list val) (Φ : val → iProp Σ) : iProp Σ :=
   match xs with
diff --git a/exercises/lang.v b/exercises/lang.v
index 44a7968..9a6b426 100644
--- a/exercises/lang.v
+++ b/exercises/lang.v
@@ -14,7 +14,7 @@ From iris.heap_lang Require Import lang notation spawn par.
   and it is a call-by-value language.
 
   The syntax for HeapLang is fairly standard, but there are some quirks
-  as we are working inside Coq. As the features of HeapLang are fairly
+  as we are working inside Rocq. As the features of HeapLang are fairly
   standard, the focus in this chapter is mainly on showcasing the syntax
   of the language through simple examples.
 *)
@@ -39,7 +39,7 @@ From iris.heap_lang Require Import lang notation spawn par.
   the tutorial, but it can optionally be installed for this chapter. To
   install it, run:
 
-    <<opam install coq-iris-unstable>>
+    <<opam install rocq-iris-unstable>>
 
   This also updates Iris to a development version. To access the
   interpreter, uncomment the import below.
@@ -73,7 +73,7 @@ Example arith : expr :=
 (**
   If the interpreter was installed, the expression can now be executed
   using [(exec 10 arith)], where [10] is the amount of fuel. To evaluate
-  the execution inside Coq, we can use the [Compute] command. Uncomment
+  the execution inside Rocq, we can use the [Compute] command. Uncomment
   the command below to see this in action.
 *)
 (* Compute (exec 10 arith). *)
diff --git a/exercises/ofe.v b/exercises/ofe.v
index 086e979..0882efb 100644
--- a/exercises/ofe.v
+++ b/exercises/ofe.v
@@ -245,7 +245,7 @@ Fail CoFixpoint repeat_with_sep (l : list nat) (x : nat) : stream :=
   sapp l (SCons x (repeat_with_sep l x)).
 
 (**
-  But this still fails with the same error. This is because Coq uses a
+  But this still fails with the same error. This is because Rocq uses a
   simple syntactic check to validate co-fixpoint definitions.
 
   To satisfy this check, we are forced to syntactically produce at least
diff --git a/exercises/pure.v b/exercises/pure.v
index b141c7c..859e5e2 100644
--- a/exercises/pure.v
+++ b/exercises/pure.v
@@ -16,12 +16,12 @@ Local Notation "Q ⊢ P" := (Q ⊢@{iPropI Σ} P).
 (** * Pure Propositions *)
 
 (**
-  The implementation of Iris in Coq has a unique class of propositions
-  called `pure'. This class arises from the fact that Coq propositions
-  can be embedded into the logic of Iris. Any Coq proposition [φ : Prop]
+  The implementation of Iris in Rocq has a unique class of propositions
+  called `pure'. This class arises from the fact that Rocq propositions
+  can be embedded into the logic of Iris. Any Rocq proposition [φ : Prop]
   can be turned into an Iris proposition through the pure embedding
   [⌜φ⌝ : iProp Σ]. This allows us to piggyback on much of the
-  functionality and theory developed for the logic of Coq. The
+  functionality and theory developed for the logic of Rocq. The
   proposition [⌜φ⌝] is thus an Iris proposition, and we can use it as we
   would any other Iris proposition.
 *)
@@ -34,11 +34,11 @@ Qed.
 
 (**
   A pure proposition is then any Iris proposition [P] for which there
-  exists a Coq proposition [φ], such that [P ⊣⊢ ⌜φ⌝].
+  exists a Rocq proposition [φ], such that [P ⊣⊢ ⌜φ⌝].
 
   Pure propositions can be introduced using [iPureIntro]. This exits the
   Iris Proof Mode, throwing away the spatial context and turns the
-  proposition into a Coq proposition.
+  proposition into a Rocq proposition.
 *)
 Lemma eq_5_5 : ⊢ ⌜5 = 5⌝.
 Proof.
@@ -48,7 +48,7 @@ Qed.
 
 (**
   To eliminate a pure proposition, we can use the specialization pattern
-  ["%_"]. This adds the proposition to the non-spatial context as a Coq
+  ["%_"]. This adds the proposition to the non-spatial context as a Rocq
   proposition.
 *)
 Lemma eq_elm {A} (P : A → iProp Σ) (x y : A) : ⌜x = y⌝ -∗ P x -∗ P y.
@@ -110,12 +110,12 @@ Qed.
   The pure embedding allows us to state an important property, namely
   soundness. Soundness is proved in the [uPred_primitive.pure_soundness]
   lemma stating: [∀ φ, (True ⊢ ⌜φ⌝) → φ]. This means that anything
-  proved inside the Iris logic is as true as anything proved in Coq.
+  proved inside the Iris logic is as true as anything proved in Rocq.
 *)
 
 (**
-  [⌜_⌝] turns Coq propositions into Iris propositions, while [⊢ _] turns
-  Iris propositions into Coq propositions. These operations are not
+  [⌜_⌝] turns Rocq propositions into Iris propositions, while [⊢ _] turns
+  Iris propositions into Rocq propositions. These operations are not
   inverses, but they are related.
 *)
 Lemma pure_adj1 (φ : Prop) : φ → ⊢ ⌜φ⌝.
diff --git a/exercises/resource_algebra.v b/exercises/resource_algebra.v
index c0d2e33..8bfa0ca 100644
--- a/exercises/resource_algebra.v
+++ b/exercises/resource_algebra.v
@@ -70,7 +70,7 @@ From iris.heap_lang Require Import lang proofmode notation.
 
   Finally, the core, written [pcore x] for a resource [x], is a partial
   function which extracts exactly the _shareable_ part of a resource. We
-  handle partiality in Coq by letting the core return an option. We
+  handle partiality in Rocq by letting the core return an option. We
   write [pcore x = Some y] to mean that the shareable part of resource
   [x] is [y]. Similarly, we write [pcore x = None] to mean that [x] has
   no shareable part. For resources [x] that are entirely shareable, we
@@ -875,7 +875,7 @@ Section ghost.
 *)
 
 (* ----------------------------------------------------------------- *)
-(** ** Accessing Resource Algebras in Coq *)
+(** ** Accessing Resource Algebras in Rocq *)
 
 (**
   To use a resource algebra inside the Iris logic, we first need to make
@@ -886,7 +886,7 @@ Section ghost.
   However, we may put _restrictions_ on [Σ] to specify that the list
   must contain some specific resource algebra of our choosing. The
   typeclass [inG Σ R] expresses that the resource algebra [R] is in the
-  [G]lobal list of resource algebras [Σ]. If we add this to the Coq
+  [G]lobal list of resource algebras [Σ]. If we add this to the Rocq
   Context, then we may assume that [Σ] contains [R], allowing us to use
   [R] inside the logic.
 
@@ -900,7 +900,7 @@ Context `{!inG Σ (exclR unitO)}.
 (**
   Similarly, if we want to use the resource algebra of discardable
   fractions, we assert that [Σ] must contain [dfracR] – the name of the
-  resource algebra in Coq.
+  resource algebra in Rocq.
 *)
 
 Context `{!inG Σ dfracR}.
@@ -910,7 +910,7 @@ Context `{!inG Σ dfracR}.
   typeclasses so that they do not have to expose the details of the
   resource algebras to clients. For instance, the [spawn] library
   includes its required resource algebras in the [spawnG Σ] typeclass.
-  As such, adding this to the Coq Context makes the resource algebras
+  As such, adding this to the Rocq Context makes the resource algebras
   required by [spawn] available.
 *)
 
diff --git a/exercises/specifications.v b/exercises/specifications.v
index 3c64bd6..9737e88 100644
--- a/exercises/specifications.v
+++ b/exercises/specifications.v
@@ -62,7 +62,7 @@ Proof.
   *)
   wp_op.
   (**
-    Note that the expression [#2 * #3] turned into [#(2 * 3)] – the Coq
+    Note that the expression [#2 * #3] turned into [#(2 * 3)] – the Rocq
     expression [2 * 3] is treated as a value in HeapLang.
 
     In particular, [wp_op] has here applied three underlying rules:
@@ -500,7 +500,7 @@ Qed.
   Secondly, specifications written in terms of Hoare triples are usually
   easier to read, as they explicitly name what must be obtained before
   the program can be executed. Finally, proving Hoare triples directly
-  can be quite awkward and burdensome, especially in Coq.
+  can be quite awkward and burdensome, especially in Rocq.
 *)
 
 (* ================================================================= *)
diff --git a/flake.nix b/flake.nix
index 4b12397..2fbd274 100644
--- a/flake.nix
+++ b/flake.nix
@@ -16,8 +16,8 @@
         buildInputs = with pkgs; [
           rocq-core
           rocqPackages.stdlib
-          rocqPackages.stdpp
-          rocqPackages.iris
+          # rocqPackages.stdpp
+          # rocqPackages.iris
           rocqPackages.vsrocq-language-server
           gawk
           git
diff --git a/coqdocjs/.gitignore b/rocqdocjs/.gitignore
similarity index 95%
rename from coqdocjs/.gitignore
rename to rocqdocjs/.gitignore
index 8efb29d..b43e727 100644
--- a/coqdocjs/.gitignore
+++ b/rocqdocjs/.gitignore
@@ -21,7 +21,7 @@
 *.vok
 *.vos
 .DS_Store
-.coq-native/
+.rocq-native/
 .csdp.cache
 .lia.cache
 .nia.cache
diff --git a/coqdocjs/LICENSE b/rocqdocjs/LICENSE
similarity index 100%
rename from coqdocjs/LICENSE
rename to rocqdocjs/LICENSE
diff --git a/coqdocjs/Makefile.doc b/rocqdocjs/Makefile.doc
similarity index 56%
rename from coqdocjs/Makefile.doc
rename to rocqdocjs/Makefile.doc
index a93fe5a..8e46080 100644
--- a/coqdocjs/Makefile.doc
+++ b/rocqdocjs/Makefile.doc
@@ -1,19 +1,19 @@
-COQDOCJS_DIR ?= coqdocjs
-EXTRA_DIR = $(COQDOCJS_DIR)/extra
-COQDOCFLAGS ?= \
+ROCQDOCJS_DIR ?= rocqdocjs
+EXTRA_DIR = $(ROCQDOCJS_DIR)/extra
+ROCQDOCFLAGS ?= \
   --toc --toc-depth 2 --html --interpolate \
   --index indexpage --no-lib-name --parse-comments \
   --with-header $(EXTRA_DIR)/header.html --with-footer $(EXTRA_DIR)/footer.html
-export COQDOCFLAGS
-COQMAKEFILE ?= Makefile.coq
-COQDOCJS_LN ?= false
+export ROCQDOCFLAGS
+ROCQMAKEFILE ?= Makefile.rocq
+ROCQDOCJS_LN ?= false
 
-coqdoc: $(COQMAKEFILE)
+rocqdoc: $(ROCQMAKEFILE)
 	$(MAKE) -f $^ html
-ifeq ($(COQDOCJS_LN),true)
+ifeq ($(ROCQDOCJS_LN),true)
 	ln -sf ../$(EXTRA_DIR)/resources html
 else
 	cp -R $(EXTRA_DIR)/resources html
 endif
 
-.PHONY: coqdoc
+.PHONY: rocqdoc
diff --git a/rocqdocjs/README.md b/rocqdocjs/README.md
new file mode 100644
index 0000000..9e160e3
--- /dev/null
+++ b/rocqdocjs/README.md
@@ -0,0 +1,46 @@
+# RocqdocJS
+
+RocqdocJS is a little script to dynamically improve the rocqdoc output.
+The result can be seen here:
+
+<https://www.ps.uni-saarland.de/autosubst/doc/Ssr.POPLmark.html>
+
+It offers the following features:
+
+- Customizable Unicode display:
+ It only changes the display, copy-paste from the website produces pure ASCII.
+ It only replaces complete identifiers or notation tokens, possibly terminated by numbers or apostrophes.
+ It does not replace randomly, like in "omega." or "tauto."
+ To add new symbols, edit [config.js](extra/resources/config.js).
+- Proof hiding:
+ All proofs longer than one line are hidden by default. They can be uncovered by clicking on "Proof...".
+
+All of this works with the ordinary rocqdoc, by asking rocqdoc to use a header file including the javascript files and some custom CSS.
+
+## Usage
+
+1. Clone this repository as a subdirectory or submodule;
+2. Include [Makefile.doc] in your `Makefile`, or copy it as, e.g., `Makefile.rocq.local`;
+3. Run `make rocqdoc` to build documentations.
+
+A minimal example is shown [here](example).
+
+### Environment Variables
+
+Name | Usage | Default
+---|---|---
+`ROCQDOCFLAGS` | Override the flags passed to `rocqdoc` | see [Makefile.doc]
+`ROCQDOCEXTRAFLAGS` | Extend the flags passed to `rocqdoc` | empty
+`ROCQDOCJS_LN` | If set to `true` then symlink resource files; otherwise copy | `false`
+`ROCQDOCJS_DIR` | Folder containing RocqdocJS | `rocqdocjs`
+`ROCQMAKEFILE` | Makefile generated by `rocq_makefile` | `Makefile.rocq`
+
+## Files
+
+- [Makefile.doc]: a generic Makefile setup that calls rocqc and rocqdoc with the right parameters
+- [config.js](extra/resources/config.js): contains the unicode replacement table
+- [rocqdoc.css](extra/resources/rocqdoc.css): a replacement for the default Rocqdoc CSS style. Can be removed to use the default style
+- [rocqdocjs.js](extra/resources/rocqdocjs.js) and [rocqdocjs.css](extra/resources/rocqdocjs.css): the script rewriting the DOM and adding the dynamic features with a corresponding CSS style
+- [header.html](extra/header.html) and [footer.html](extra/footer.html): custom header and footer files used in every generated html file
+
+[Makefile.doc]: Makefile.doc
diff --git a/rocqdocjs/example/.gitignore b/rocqdocjs/example/.gitignore
new file mode 100644
index 0000000..c94f8be
--- /dev/null
+++ b/rocqdocjs/example/.gitignore
@@ -0,0 +1,3 @@
+Makefile.rocq
+Makefile.rocq.conf
+html/
diff --git a/rocqdocjs/example/Makefile b/rocqdocjs/example/Makefile
new file mode 100644
index 0000000..52516ce
--- /dev/null
+++ b/rocqdocjs/example/Makefile
@@ -0,0 +1,21 @@
+ROCQMAKEFILE ?= Makefile.rocq
+ROCQDOCEXTRAFLAGS = -s
+ROCQDOCJS_LN = true
+ROCQ_PROJ ?= _RocqProject
+
+all: $(ROCQMAKEFILE)
+	$(MAKE) -f $^ $@
+
+clean: $(ROCQMAKEFILE)
+	$(MAKE) -f $^ cleanall
+	$(RM) $^ $^.conf
+
+$(ROCQMAKEFILE): $(ROCQ_PROJ)
+	$(ROCQBIN)rocq_makefile -f $^ -o $@
+
+force $(ROCQ_PROJ) Makefile: ;
+
+%: $(ROCQMAKEFILE) force
+	@+$(MAKE) -f $< $@
+
+.PHONY: clean all force
diff --git a/coqdocjs/example/Makefile.coq.local b/rocqdocjs/example/Makefile.coq.local
similarity index 100%
rename from coqdocjs/example/Makefile.coq.local
rename to rocqdocjs/example/Makefile.coq.local
diff --git a/rocqdocjs/example/README.md b/rocqdocjs/example/README.md
new file mode 100644
index 0000000..e5a3269
--- /dev/null
+++ b/rocqdocjs/example/README.md
@@ -0,0 +1,5 @@
+# RocqdocJS Usage Example
+
+This folder contains a minimal example to use RocqdocJS in your project.
+
+You can build the docs with `make rocqdoc`.
diff --git a/coqdocjs/example/_CoqProject b/rocqdocjs/example/_CoqProject
similarity index 100%
rename from coqdocjs/example/_CoqProject
rename to rocqdocjs/example/_CoqProject
diff --git a/coqdocjs/example/a.v b/rocqdocjs/example/a.v
similarity index 100%
rename from coqdocjs/example/a.v
rename to rocqdocjs/example/a.v
diff --git a/coqdocjs/example/coqdocjs/Makefile.doc b/rocqdocjs/example/coqdocjs/Makefile.doc
similarity index 100%
rename from coqdocjs/example/coqdocjs/Makefile.doc
rename to rocqdocjs/example/coqdocjs/Makefile.doc
diff --git a/coqdocjs/example/coqdocjs/extra b/rocqdocjs/example/coqdocjs/extra
similarity index 100%
rename from coqdocjs/example/coqdocjs/extra
rename to rocqdocjs/example/coqdocjs/extra
diff --git a/rocqdocjs/extra/footer.html b/rocqdocjs/extra/footer.html
new file mode 100644
index 0000000..ea34896
--- /dev/null
+++ b/rocqdocjs/extra/footer.html
@@ -0,0 +1,9 @@
+</div>
+<div id="footer">
+  Generated by <a href="http://rocq.inria.fr/">rocqdoc</a> and improved with <a
+    href="https://github.com/rocq-community/rocqdocjs">RocqdocJS</a>
+</div>
+</div>
+</body>
+
+</html>
\ No newline at end of file
diff --git a/rocqdocjs/extra/header.html b/rocqdocjs/extra/header.html
new file mode 100644
index 0000000..581ac04
--- /dev/null
+++ b/rocqdocjs/extra/header.html
@@ -0,0 +1,28 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+
+<head>
+  <meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
+  <link href="resources/rocqdoc.css" rel="stylesheet" type="text/css" />
+  <link href="resources/rocqdocjs.css" rel="stylesheet" type="text/css" />
+  <script type="text/javascript" src="resources/config.js"></script>
+  <script type="text/javascript" src="resources/rocqdocjs.js"></script>
+</head>
+
+<body onload="document.getElementById('content').focus()">
+  <div id="header">
+    <span class="left">
+      <span class="modulename">
+        <script> document.write(document.title) </script>
+      </span>
+    </span>
+
+    <span class="button" id="toggle-proofs"></span>
+
+    <span class="right">
+      <a href="./indexpage.html"> Index </a>
+      <a href="./toc.html"> Table of Contents </a>
+    </span>
+  </div>
+  <div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
+    <div id="main">
\ No newline at end of file
diff --git a/coqdocjs/extra/resources/config.js b/rocqdocjs/extra/resources/config.js
similarity index 89%
rename from coqdocjs/extra/resources/config.js
rename to rocqdocjs/extra/resources/config.js
index 72be613..bd460ec 100644
--- a/coqdocjs/extra/resources/config.js
+++ b/rocqdocjs/extra/resources/config.js
@@ -1,6 +1,6 @@
-var coqdocjs = coqdocjs || {};
+var rocqdocjs = rocqdocjs || {};
 
-coqdocjs.repl = {
+rocqdocjs.repl = {
     "forall": "∀",
     "exists": "∃",
     "~": "¬",
@@ -56,7 +56,7 @@ coqdocjs.repl = {
     "Xi": "Ξ"
 };
 
-coqdocjs.subscr = {
+rocqdocjs.subscr = {
   "0" : "₀",
   "1" : "₁",
   "2" : "₂",
@@ -69,4 +69,4 @@ coqdocjs.subscr = {
   "9" : "₉",
 };
 
-coqdocjs.replInText = ["==>","<=>", "=>", "->", "<-", ":="];
+rocqdocjs.replInText = ["==>","<=>", "=>", "->", "<-", ":="];
diff --git a/coqdocjs/extra/resources/coqdoc.css b/rocqdocjs/extra/resources/coqdoc.css
similarity index 100%
rename from coqdocjs/extra/resources/coqdoc.css
rename to rocqdocjs/extra/resources/coqdoc.css
diff --git a/coqdocjs/extra/resources/coqdocjs.css b/rocqdocjs/extra/resources/coqdocjs.css
similarity index 100%
rename from coqdocjs/extra/resources/coqdocjs.css
rename to rocqdocjs/extra/resources/coqdocjs.css
diff --git a/coqdocjs/extra/resources/coqdocjs.js b/rocqdocjs/extra/resources/coqdocjs.js
similarity index 95%
rename from coqdocjs/extra/resources/coqdocjs.js
rename to rocqdocjs/extra/resources/coqdocjs.js
index 7ff5698..3ebeda5 100644
--- a/coqdocjs/extra/resources/coqdocjs.js
+++ b/rocqdocjs/extra/resources/coqdocjs.js
@@ -1,4 +1,4 @@
-var coqdocjs = coqdocjs || {};
+var rocqdocjs = rocqdocjs || {};
 (function(){
 
 function replace(s){
@@ -7,14 +7,14 @@ function replace(s){
     return replace(m[1])+"'";
   } else if (m = s.match(/^([A-Za-z]+)_?(\d+)$/)) {
     return replace(m[1])+m[2].replace(/\d/g, function(d){
-      if (coqdocjs.subscr.hasOwnProperty(d)) {
-        return coqdocjs.subscr[d];
+      if (rocqdocjs.subscr.hasOwnProperty(d)) {
+        return rocqdocjs.subscr[d];
       } else {
         return d;
       }
     });
-  } else if (coqdocjs.repl.hasOwnProperty(s)){
-    return coqdocjs.repl[s]
+  } else if (rocqdocjs.repl.hasOwnProperty(s)){
+    return rocqdocjs.repl[s]
   } else {
     return s;
   }
@@ -25,7 +25,7 @@ function toArray(nl){
 }
 
 function replInTextNodes() {
-  coqdocjs.replInText.forEach(function(toReplace){
+  rocqdocjs.replInText.forEach(function(toReplace){
     toArray(document.getElementsByClassName("code")).concat(toArray(document.getElementsByClassName("inlinecode"))).forEach(function(elem){
       toArray(elem.childNodes).forEach(function(node){
         if (node.nodeType != Node.TEXT_NODE) return;
@@ -185,5 +185,5 @@ function postprocess(){
 fixTitle();
 document.addEventListener('DOMContentLoaded', postprocess);
 
-coqdocjs.toggleProofs = toggleProofs;
+rocqdocjs.toggleProofs = toggleProofs;
 })();
diff --git a/theories/basics.v b/theories/basics.v
index d04bb2b..44fdffd 100644
--- a/theories/basics.v
+++ b/theories/basics.v
@@ -51,7 +51,7 @@ From iris.proofmode Require Import proofmode.
 *)
 
 (* ================================================================= *)
-(** ** Iris in Coq *)
+(** ** Iris in Rocq *)
 
 (**
   The type of propositions in Iris is [iProp Σ]. All proofs in Iris are
@@ -67,17 +67,17 @@ Section proofs.
 Context {Σ: gFunctors}.
 
 (**
-  Iris defines two Coq propositions for proving Iris propositions:
+  Iris defines two Rocq propositions for proving Iris propositions:
   - [⊢ P] asks whether [P] holds with no assumptions
   - [P ⊢ Q] asks whether [Q] holds assuming [P]
 
-  Iris is built on top of Coq, so to smoothen the experience, we will be
+  Iris is built on top of Rocq, so to smoothen the experience, we will be
   working with the Iris Proof Mode (IPM). The practical implication of
   this is that we get a new context, called the spatial context, in
   addition to the usual context, now called the non-spatial context.
   Hypotheses from both contexts can be used to prove the goal.
 
-  The regular Coq tactics can still be used when we work within the
+  The regular Rocq tactics can still be used when we work within the
   non-spatial context, but, in general, we shall use new tactics that
   work natively with the spatial context. These new tactics start with
   'i', and since many of them simply 'lift' the regular tactics to also
@@ -85,7 +85,7 @@ Context {Σ: gFunctors}.
   the 'i' prefixed. For instance, instead of [intros H] we use
   [iIntros "H"], and instead of [apply H] we use [iApply "H"]. Note that
   identifiers for hypotheses in the spatial context are strings, instead
-  of the usual Coq identifiers.
+  of the usual Rocq identifiers.
 
   To see this in action we will prove the statement [P ⊢ P], for all
   [P].
@@ -111,12 +111,12 @@ Qed.
 (** *** Technical Details *)
 
 (**
-  In Coq, the context and the goal is a sequent (we use [⊢ₓ] for
-  the Coq entailment to distinguish it from the Iris entailment [⊢]):
+  In Rocq, the context and the goal is a sequent (we use [⊢ₓ] for
+  the Rocq entailment to distinguish it from the Iris entailment [⊢]):
 
                     [H₁ : Φ₁, ..., Hₙ : Φₙ ⊢ₓ Ψ]
 
-  Here, the left-hand side of the Coq entailment [⊢ₓ] is the
+  Here, the left-hand side of the Rocq entailment [⊢ₓ] is the
   (non-spatial) context and the right-hand side is the goal. This
   sequent is equivalent to the entailment [Φ₁ ∧ ... ∧ Φₙ ⊢ₓ Ψ].
 
@@ -128,17 +128,17 @@ Qed.
   However, as Iris is a separation logic, this is equivalent to the
   entailment [Φ₁ ∗ ... ∗ Φₙ ⊢ Ψ].
 
-  Technically, since Iris is built on top of Coq, proving an Iris
-  entailment in Coq corresponds to proving [⊢ₓ (P ⊢ Q)]. In other
-  words, the spatial context is part of the Coq goal. This is the reason
-  why the regular Coq tactics no longer suffice. The new tactics work
+  Technically, since Iris is built on top of Rocq, proving an Iris
+  entailment in Rocq corresponds to proving [⊢ₓ (P ⊢ Q)]. In other
+  words, the spatial context is part of the Rocq goal. This is the reason
+  why the regular Rocq tactics no longer suffice. The new tactics work
   with both the non-spatial and the spatial contexts.
 *)
 
 (**
   Iris propositions include many of the usual logical connectives such
   as conjunction [P ∧ Q]. As such, Iris uses a notation scope to
-  overload the usual logical notation in Coq. This scope is delimited by
+  overload the usual logical notation in Rocq. This scope is delimited by
   [I] and bound to [iProp Σ]. Hence, you may need to wrap your
   propositions in [(_)%I] to use the notations.
 *)
@@ -228,8 +228,8 @@ Lemma modus_ponens (P Q : iProp Σ) : P -∗ (P -∗ Q) -∗ Q.
 Qed.
 
 (**
-  Just as with Coq tactics, Iris allows nesting of introduction
-  patterns. In fact, like Coq, Iris supports patterns of the form
+  Just as with Rocq tactics, Iris allows nesting of introduction
+  patterns. In fact, like Rocq, Iris supports patterns of the form
   [(H1 & .. & H2 & H3)] as a shorthand for [[H1 .. [H2 H3] ..]].
 
   Exercise: try to use an introduction with a pattern of parentheses to
@@ -312,7 +312,7 @@ Admitted.
 END TEMPLATE *)
 
 (**
-  Disjunctions [∨] are treated just like disjunctions in Coq. The
+  Disjunctions [∨] are treated just like disjunctions in Rocq. The
   introduction pattern [[ _ | _ ]] allows us to eliminate a disjunction,
   while the tactics [iLeft] and [iRight] let us introduce them.
 
@@ -359,7 +359,7 @@ Admitted.
 END TEMPLATE *)
 
 (**
-  Iris has existential and universal quantifiers over any Coq type.
+  Iris has existential and universal quantifiers over any Rocq type.
   Existential quantifiers are proved using the [iExists] tactic, using
   the same syntax as for [exists]. Elimination of existentials is done
   through the pattern ["[%_ _]"] or as part of a ["(_&..&_)"] with a [%]
@@ -389,7 +389,7 @@ Admitted.
 END TEMPLATE *)
 
 (**
-  Likewise, forall quantification works almost as in Coq. To introduce
+  Likewise, forall quantification works almost as in Rocq. To introduce
   universally quantified variables, you can either use [iIntros (x y z)]
   or [iIntros "%x %y %z"]. These patterns are interchangeable. To
   specify the parameters of hypotheses, we write
diff --git a/theories/custom_ra.v b/theories/custom_ra.v
index 1e89f9f..334975e 100644
--- a/theories/custom_ra.v
+++ b/theories/custom_ra.v
@@ -130,7 +130,7 @@ Qed.
 
 (**
   The final step is to package this into a CMRA structure, allowing us
-  to use the resource algebra in proofs (using Coq's Context mechanism).
+  to use the resource algebra in proofs (using Rocq's Context mechanism).
 *)
 Canonical Structure stateR := discreteR state state_ra_mixin.
 
diff --git a/theories/gr_predicates.v b/theories/gr_predicates.v
index 333ce03..b8ee3ce 100644
--- a/theories/gr_predicates.v
+++ b/theories/gr_predicates.v
@@ -6,12 +6,12 @@ From iris.heap_lang Require Import lang proofmode notation.
 
 (**
   In the Linked List chapter, we defined a representation predicate for
-  linked lists using Coq's Fixpoint mechanism. In this chapter, we
+  linked lists using Rocq's Fixpoint mechanism. In this chapter, we
   present an alternative approach to defining representation predicates,
   which instead uses fixpoints of predicates. The high-level point to
   notice is that we can define fixpoints of monotone functions on Iris
   predicates, much in the same way as one can define fixpoints of
-  monotone function on Coq predicates. Later on, we will discuss
+  monotone function on Rocq predicates. Later on, we will discuss
   different kinds of fixpoints in more detail.
 *)
 
@@ -20,9 +20,10 @@ Context `{!heapGS Σ}.
 
 (**
   As we have already seen, we can define a predicate for linked lists
-  representing a list of specific values, using Coq's notion of fixpoint
-  for the inductive Coq type [list val].
+  representing a list of specific values, using Rocq's notion of fixpoint
+  for the inductive Rocq type [list val].
 *)
+
 Fixpoint is_list_of (v : val) (xs : list val) : iProp Σ :=
   match xs with
   | [] => ⌜v = NONEV⌝
@@ -33,7 +34,7 @@ Fixpoint is_list_of (v : val) (xs : list val) : iProp Σ :=
   However, sometimes we don't care about the exact list and instead, we
   only want to know that each value of the list satisfies some
   predicate. This can be captured by using a helper predicate [all]
-  expressing that all elements of a Coq list satisfy a predicate.
+  expressing that all elements of a Rocq list satisfy a predicate.
 *)
 Fixpoint all (xs : list val) (Φ : val → iProp Σ) : iProp Σ :=
   match xs with
diff --git a/theories/lang.v b/theories/lang.v
index 44a7968..9a6b426 100644
--- a/theories/lang.v
+++ b/theories/lang.v
@@ -14,7 +14,7 @@ From iris.heap_lang Require Import lang notation spawn par.
   and it is a call-by-value language.
 
   The syntax for HeapLang is fairly standard, but there are some quirks
-  as we are working inside Coq. As the features of HeapLang are fairly
+  as we are working inside Rocq. As the features of HeapLang are fairly
   standard, the focus in this chapter is mainly on showcasing the syntax
   of the language through simple examples.
 *)
@@ -39,7 +39,7 @@ From iris.heap_lang Require Import lang notation spawn par.
   the tutorial, but it can optionally be installed for this chapter. To
   install it, run:
 
-    <<opam install coq-iris-unstable>>
+    <<opam install rocq-iris-unstable>>
 
   This also updates Iris to a development version. To access the
   interpreter, uncomment the import below.
@@ -73,7 +73,7 @@ Example arith : expr :=
 (**
   If the interpreter was installed, the expression can now be executed
   using [(exec 10 arith)], where [10] is the amount of fuel. To evaluate
-  the execution inside Coq, we can use the [Compute] command. Uncomment
+  the execution inside Rocq, we can use the [Compute] command. Uncomment
   the command below to see this in action.
 *)
 (* Compute (exec 10 arith). *)
diff --git a/theories/ofe.v b/theories/ofe.v
index b7e91f5..cc61e3f 100644
--- a/theories/ofe.v
+++ b/theories/ofe.v
@@ -274,7 +274,7 @@ Fail CoFixpoint repeat_with_sep (l : list nat) (x : nat) : stream :=
   sapp l (SCons x (repeat_with_sep l x)).
 
 (**
-  But this still fails with the same error. This is because Coq uses a
+  But this still fails with the same error. This is because Rocq uses a
   simple syntactic check to validate co-fixpoint definitions.
 
   To satisfy this check, we are forced to syntactically produce at least
diff --git a/theories/pure.v b/theories/pure.v
index 9f102da..e522e66 100644
--- a/theories/pure.v
+++ b/theories/pure.v
@@ -16,12 +16,12 @@ Local Notation "Q ⊢ P" := (Q ⊢@{iPropI Σ} P).
 (** * Pure Propositions *)
 
 (**
-  The implementation of Iris in Coq has a unique class of propositions
-  called `pure'. This class arises from the fact that Coq propositions
-  can be embedded into the logic of Iris. Any Coq proposition [φ : Prop]
+  The implementation of Iris in Rocq has a unique class of propositions
+  called `pure'. This class arises from the fact that Rocq propositions
+  can be embedded into the logic of Iris. Any Rocq proposition [φ : Prop]
   can be turned into an Iris proposition through the pure embedding
   [⌜φ⌝ : iProp Σ]. This allows us to piggyback on much of the
-  functionality and theory developed for the logic of Coq. The
+  functionality and theory developed for the logic of Rocq. The
   proposition [⌜φ⌝] is thus an Iris proposition, and we can use it as we
   would any other Iris proposition.
 *)
@@ -34,11 +34,11 @@ Qed.
 
 (**
   A pure proposition is then any Iris proposition [P] for which there
-  exists a Coq proposition [φ], such that [P ⊣⊢ ⌜φ⌝].
+  exists a Rocq proposition [φ], such that [P ⊣⊢ ⌜φ⌝].
 
   Pure propositions can be introduced using [iPureIntro]. This exits the
   Iris Proof Mode, throwing away the spatial context and turns the
-  proposition into a Coq proposition.
+  proposition into a Rocq proposition.
 *)
 Lemma eq_5_5 : ⊢ ⌜5 = 5⌝.
 Proof.
@@ -48,7 +48,7 @@ Qed.
 
 (**
   To eliminate a pure proposition, we can use the specialization pattern
-  ["%_"]. This adds the proposition to the non-spatial context as a Coq
+  ["%_"]. This adds the proposition to the non-spatial context as a Rocq
   proposition.
 *)
 Lemma eq_elm {A} (P : A → iProp Σ) (x y : A) : ⌜x = y⌝ -∗ P x -∗ P y.
@@ -110,12 +110,12 @@ Qed.
   The pure embedding allows us to state an important property, namely
   soundness. Soundness is proved in the [uPred_primitive.pure_soundness]
   lemma stating: [∀ φ, (True ⊢ ⌜φ⌝) → φ]. This means that anything
-  proved inside the Iris logic is as true as anything proved in Coq.
+  proved inside the Iris logic is as true as anything proved in Rocq.
 *)
 
 (**
-  [⌜_⌝] turns Coq propositions into Iris propositions, while [⊢ _] turns
-  Iris propositions into Coq propositions. These operations are not
+  [⌜_⌝] turns Rocq propositions into Iris propositions, while [⊢ _] turns
+  Iris propositions into Rocq propositions. These operations are not
   inverses, but they are related.
 *)
 Lemma pure_adj1 (φ : Prop) : φ → ⊢ ⌜φ⌝.
diff --git a/theories/resource_algebra.v b/theories/resource_algebra.v
index 918b346..e603e1a 100644
--- a/theories/resource_algebra.v
+++ b/theories/resource_algebra.v
@@ -70,7 +70,7 @@ From iris.heap_lang Require Import lang proofmode notation.
 
   Finally, the core, written [pcore x] for a resource [x], is a partial
   function which extracts exactly the _shareable_ part of a resource. We
-  handle partiality in Coq by letting the core return an option. We
+  handle partiality in Rocq by letting the core return an option. We
   write [pcore x = Some y] to mean that the shareable part of resource
   [x] is [y]. Similarly, we write [pcore x = None] to mean that [x] has
   no shareable part. For resources [x] that are entirely shareable, we
@@ -908,7 +908,7 @@ Section ghost.
 *)
 
 (* ----------------------------------------------------------------- *)
-(** ** Accessing Resource Algebras in Coq *)
+(** ** Accessing Resource Algebras in Rocq *)
 
 (**
   To use a resource algebra inside the Iris logic, we first need to make
@@ -919,7 +919,7 @@ Section ghost.
   However, we may put _restrictions_ on [Σ] to specify that the list
   must contain some specific resource algebra of our choosing. The
   typeclass [inG Σ R] expresses that the resource algebra [R] is in the
-  [G]lobal list of resource algebras [Σ]. If we add this to the Coq
+  [G]lobal list of resource algebras [Σ]. If we add this to the Rocq
   Context, then we may assume that [Σ] contains [R], allowing us to use
   [R] inside the logic.
 
@@ -933,7 +933,7 @@ Context `{!inG Σ (exclR unitO)}.
 (**
   Similarly, if we want to use the resource algebra of discardable
   fractions, we assert that [Σ] must contain [dfracR] – the name of the
-  resource algebra in Coq.
+  resource algebra in Rocq.
 *)
 
 Context `{!inG Σ dfracR}.
@@ -943,7 +943,7 @@ Context `{!inG Σ dfracR}.
   typeclasses so that they do not have to expose the details of the
   resource algebras to clients. For instance, the [spawn] library
   includes its required resource algebras in the [spawnG Σ] typeclass.
-  As such, adding this to the Coq Context makes the resource algebras
+  As such, adding this to the Rocq Context makes the resource algebras
   required by [spawn] available.
 *)
 
diff --git a/theories/specifications.v b/theories/specifications.v
index 9298106..8efe1c9 100644
--- a/theories/specifications.v
+++ b/theories/specifications.v
@@ -62,7 +62,7 @@ Proof.
   *)
   wp_op.
   (**
-    Note that the expression [#2 * #3] turned into [#(2 * 3)] – the Coq
+    Note that the expression [#2 * #3] turned into [#(2 * 3)] – the Rocq
     expression [2 * 3] is treated as a value in HeapLang.
 
     In particular, [wp_op] has here applied three underlying rules:
@@ -528,7 +528,7 @@ Qed.
   Secondly, specifications written in terms of Hoare triples are usually
   easier to read, as they explicitly name what must be obtained before
   the program can be executed. Finally, proving Hoare triples directly
-  can be quite awkward and burdensome, especially in Coq.
+  can be quite awkward and burdensome, especially in Rocq.
 *)
 
 (* ================================================================= *)

From e26d0827ac54eb330fc63aa0d3bee72d1946991d Mon Sep 17 00:00:00 2001
From: Serhii Khoma <sergey@nordicresults.com>
Date: Wed, 22 Jul 2026 22:12:55 +0700
Subject: [PATCH 3/8] feat: update to latest rocq -> fix "make all && make
 html"

---
 exercises/array_lock.v |  1 +
 exercises/custom_ra.v  |  1 +
 flake.nix              | 21 ++++++++++++++++++---
 theories/array_lock.v  |  1 +
 theories/custom_ra.v   |  1 +
 5 files changed, 22 insertions(+), 3 deletions(-)

diff --git a/exercises/array_lock.v b/exercises/array_lock.v
index 2fc113f..4abe985 100644
--- a/exercises/array_lock.v
+++ b/exercises/array_lock.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Import auth excl gset numbers.
+From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang Require Import lang proofmode notation par.
 
 Lemma lookup_array `{!heapGS_gen hlc Σ} l dq vs off v :
diff --git a/exercises/custom_ra.v b/exercises/custom_ra.v
index 60979ff..684df25 100644
--- a/exercises/custom_ra.v
+++ b/exercises/custom_ra.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Import cmra.
+From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang.lib Require Export par.
 From iris.heap_lang Require Import proofmode notation.
 
diff --git a/flake.nix b/flake.nix
index 2fbd274..644f2c6 100644
--- a/flake.nix
+++ b/flake.nix
@@ -14,14 +14,29 @@
     {
       devShells.${system}.default = pkgs.mkShell {
         buildInputs = with pkgs; [
-          rocq-core
-          rocqPackages.stdlib
+          # OPAM tool and build dependencies
+          opam
+          gmp
+          pkg-config
+          rsync
+          unzip
+          patch
+
+          # Rocq & language server (Commented out because installed via opam)
+          # rocq-core
+          # rocqPackages.stdlib
           # rocqPackages.stdpp
           # rocqPackages.iris
-          rocqPackages.vsrocq-language-server
+          # rocqPackages.vsrocq-language-server
+
           gawk
           git
         ];
+
+        shellHook = ''
+          # Automatically load opam environment variables if an opam switch exists
+          eval $(opam env 2>/dev/null)
+        '';
       };
 
       checks.${system}.default = pkgs.stdenv.mkDerivation {
diff --git a/theories/array_lock.v b/theories/array_lock.v
index 2fc113f..4abe985 100644
--- a/theories/array_lock.v
+++ b/theories/array_lock.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Import auth excl gset numbers.
+From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang Require Import lang proofmode notation par.
 
 Lemma lookup_array `{!heapGS_gen hlc Σ} l dq vs off v :
diff --git a/theories/custom_ra.v b/theories/custom_ra.v
index 334975e..e73a1ef 100644
--- a/theories/custom_ra.v
+++ b/theories/custom_ra.v
@@ -1,4 +1,5 @@
 From iris.algebra Require Import cmra.
+From iris.base_logic.lib Require Export invariants.
 From iris.heap_lang.lib Require Export par.
 From iris.heap_lang Require Import proofmode notation.
 

From 21704b87f1c7025ca0a747f4ea8a3e749a944c71 Mon Sep 17 00:00:00 2001
From: Serhii Khoma <sergey@nordicresults.com>
Date: Wed, 22 Jul 2026 22:25:30 +0700
Subject: [PATCH 4/8] feat: update to latest rocq -> fix "make all && make
 html"

---
 rocqdocjs/example/{Makefile.coq.local => Makefile.rocq.local} | 0
 rocqdocjs/example/{_CoqProject => _RocqProject}               | 0
 rocqdocjs/example/{coqdocjs => rocqdocjs}/Makefile.doc        | 0
 rocqdocjs/example/{coqdocjs => rocqdocjs}/extra               | 0
 rocqdocjs/extra/header.html                                   | 4 +++-
 rocqdocjs/extra/resources/{coqdoc.css => rocqdoc.css}         | 0
 rocqdocjs/extra/resources/{coqdocjs.css => rocqdocjs.css}     | 2 +-
 rocqdocjs/extra/resources/{coqdocjs.js => rocqdocjs.js}       | 0
 8 files changed, 4 insertions(+), 2 deletions(-)
 rename rocqdocjs/example/{Makefile.coq.local => Makefile.rocq.local} (100%)
 rename rocqdocjs/example/{_CoqProject => _RocqProject} (100%)
 rename rocqdocjs/example/{coqdocjs => rocqdocjs}/Makefile.doc (100%)
 rename rocqdocjs/example/{coqdocjs => rocqdocjs}/extra (100%)
 rename rocqdocjs/extra/resources/{coqdoc.css => rocqdoc.css} (100%)
 rename rocqdocjs/extra/resources/{coqdocjs.css => rocqdocjs.css} (99%)
 rename rocqdocjs/extra/resources/{coqdocjs.js => rocqdocjs.js} (100%)

diff --git a/rocqdocjs/example/Makefile.coq.local b/rocqdocjs/example/Makefile.rocq.local
similarity index 100%
rename from rocqdocjs/example/Makefile.coq.local
rename to rocqdocjs/example/Makefile.rocq.local
diff --git a/rocqdocjs/example/_CoqProject b/rocqdocjs/example/_RocqProject
similarity index 100%
rename from rocqdocjs/example/_CoqProject
rename to rocqdocjs/example/_RocqProject
diff --git a/rocqdocjs/example/coqdocjs/Makefile.doc b/rocqdocjs/example/rocqdocjs/Makefile.doc
similarity index 100%
rename from rocqdocjs/example/coqdocjs/Makefile.doc
rename to rocqdocjs/example/rocqdocjs/Makefile.doc
diff --git a/rocqdocjs/example/coqdocjs/extra b/rocqdocjs/example/rocqdocjs/extra
similarity index 100%
rename from rocqdocjs/example/coqdocjs/extra
rename to rocqdocjs/example/rocqdocjs/extra
diff --git a/rocqdocjs/extra/header.html b/rocqdocjs/extra/header.html
index 581ac04..9bb4c92 100644
--- a/rocqdocjs/extra/header.html
+++ b/rocqdocjs/extra/header.html
@@ -25,4 +25,6 @@
     </span>
   </div>
   <div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
-    <div id="main">
\ No newline at end of file
+    <div id="main"></div>
+  </div>
+</body>
\ No newline at end of file
diff --git a/rocqdocjs/extra/resources/coqdoc.css b/rocqdocjs/extra/resources/rocqdoc.css
similarity index 100%
rename from rocqdocjs/extra/resources/coqdoc.css
rename to rocqdocjs/extra/resources/rocqdoc.css
diff --git a/rocqdocjs/extra/resources/coqdocjs.css b/rocqdocjs/extra/resources/rocqdocjs.css
similarity index 99%
rename from rocqdocjs/extra/resources/coqdocjs.css
rename to rocqdocjs/extra/resources/rocqdocjs.css
index d94bb58..bb0fc35 100644
--- a/rocqdocjs/extra/resources/coqdocjs.css
+++ b/rocqdocjs/extra/resources/rocqdocjs.css
@@ -109,7 +109,7 @@ html, body {
 @media only screen { /* no div with internal scrolling to allow printing of whole content */
     body {
         display: flex;
-        flex-direction: column 
+        flex-direction: column
     }
 
     #content {
diff --git a/rocqdocjs/extra/resources/coqdocjs.js b/rocqdocjs/extra/resources/rocqdocjs.js
similarity index 100%
rename from rocqdocjs/extra/resources/coqdocjs.js
rename to rocqdocjs/extra/resources/rocqdocjs.js

From 608c87a838a00241b1f9cb696ff9b17f5501d6b1 Mon Sep 17 00:00:00 2001
From: Serhii Khoma <sergey@nordicresults.com>
Date: Wed, 22 Jul 2026 22:32:32 +0700
Subject: [PATCH 5/8] feat: update to latest rocq -> update vscode ext

---
 .devcontainer/arm64/devcontainer.json  | 4 ++--
 .devcontainer/x86-64/devcontainer.json | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/.devcontainer/arm64/devcontainer.json b/.devcontainer/arm64/devcontainer.json
index 92483f5..658ba24 100644
--- a/.devcontainer/arm64/devcontainer.json
+++ b/.devcontainer/arm64/devcontainer.json
@@ -3,7 +3,7 @@
 	"image": "ghcr.io/logsem/iris-tutorial/docker-arm64",
 	"customizations": {
 		"vscode": {
-		  "extensions": ["maximedenes.vsrocq"]
+		  "extensions": ["rocq-prover.vsrocq"]
 		},
 		"settings": {
 			"terminal.integrated.profiles.linux": {
@@ -15,4 +15,4 @@
 			"terminal.integrated.defaultProfile.linux": "bash"
 		}
 	}
-}
\ No newline at end of file
+}
diff --git a/.devcontainer/x86-64/devcontainer.json b/.devcontainer/x86-64/devcontainer.json
index 68b8322..c714ac2 100644
--- a/.devcontainer/x86-64/devcontainer.json
+++ b/.devcontainer/x86-64/devcontainer.json
@@ -3,7 +3,7 @@
 	"image": "ghcr.io/logsem/iris-tutorial/docker-x86-64",
 	"customizations": {
 		"vscode": {
-		  "extensions": ["maximedenes.vsrocq"]
+		  "extensions": ["rocq-prover.vsrocq"]
 		},
 		"settings": {
 			"terminal.integrated.profiles.linux": {
@@ -15,4 +15,4 @@
 			"terminal.integrated.defaultProfile.linux": "bash"
 		}
 	}
-}
\ No newline at end of file
+}

From 946ee8e1c1de789a3ceb8bca72a02fde64f92a94 Mon Sep 17 00:00:00 2001
From: Serhii Khoma <sergey@nordicresults.com>
Date: Wed, 22 Jul 2026 23:19:22 +0700
Subject: [PATCH 6/8] feat: update to latest rocq -> dockerfiles

---
 .devcontainer/arm64/devcontainer.json  |  5 +-
 .devcontainer/x86-64/devcontainer.json |  5 +-
 .dockerignore                          |  2 +
 .github/workflows/build.yml            | 15 ++++--
 docker_image/Dockerfile                | 53 ++++++++++-----------
 docker_image/Makefile                  | 64 ++++++++++++++++++++++----
 6 files changed, 100 insertions(+), 44 deletions(-)
 create mode 100644 .dockerignore

diff --git a/.devcontainer/arm64/devcontainer.json b/.devcontainer/arm64/devcontainer.json
index 658ba24..c167ea0 100644
--- a/.devcontainer/arm64/devcontainer.json
+++ b/.devcontainer/arm64/devcontainer.json
@@ -1,6 +1,6 @@
 {
 	"name": "iris-tutorial arm64 container",
-	"image": "ghcr.io/logsem/iris-tutorial/docker-arm64",
+	"image": "ghcr.io/logsem/iris-tutorial/debian-ocaml-5.5-arm64",
 	"customizations": {
 		"vscode": {
 		  "extensions": ["rocq-prover.vsrocq"]
@@ -14,5 +14,6 @@
 			},
 			"terminal.integrated.defaultProfile.linux": "bash"
 		}
-	}
+	},
+	"remoteUser": "opam"
 }
diff --git a/.devcontainer/x86-64/devcontainer.json b/.devcontainer/x86-64/devcontainer.json
index c714ac2..87d425a 100644
--- a/.devcontainer/x86-64/devcontainer.json
+++ b/.devcontainer/x86-64/devcontainer.json
@@ -1,6 +1,6 @@
 {
 	"name": "iris-tutorial x86-64 container",
-	"image": "ghcr.io/logsem/iris-tutorial/docker-x86-64",
+	"image": "ghcr.io/logsem/iris-tutorial/debian-ocaml-5.5-x86-64",
 	"customizations": {
 		"vscode": {
 		  "extensions": ["rocq-prover.vsrocq"]
@@ -14,5 +14,6 @@
 			},
 			"terminal.integrated.defaultProfile.linux": "bash"
 		}
-	}
+	},
+	"remoteUser": "opam"
 }
diff --git a/.dockerignore b/.dockerignore
new file mode 100644
index 0000000..a0be568
--- /dev/null
+++ b/.dockerignore
@@ -0,0 +1,2 @@
+*
+!iris-tutorial.opam
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 0b8ed0d..aaa24c7 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -12,11 +12,18 @@ jobs:
   build:
     runs-on: ubuntu-latest
     container:
-      image: ghcr.io/logsem/iris-tutorial/docker-x86-64:latest
-      options: --user root
+      image: ghcr.io/logsem/iris-tutorial/debian-ocaml-5.5-x86-64
+      options: --user opam
 
     steps:
       - uses: actions/checkout@v4
-      - name: make-ci
+
+      - name: Build project
         shell: bash -l {0}
-        run: export HOME=/root; eval $(opam env); make ci -j2
+        run: |
+          # Fix for git ownership issues in containers
+          git config --global --add safe.directory /__w/iris-tutorial/iris-tutorial
+
+          # No need to export HOME=/root, we are opam
+          eval $(opam env)
+          make ci -j2
diff --git a/docker_image/Dockerfile b/docker_image/Dockerfile
index 2c7a6aa..f832975 100644
--- a/docker_image/Dockerfile
+++ b/docker_image/Dockerfile
@@ -1,35 +1,36 @@
-FROM debian:bookworm
+ARG BASE_IMAGE
+FROM ${BASE_IMAGE}
 
-RUN apt-get -y update
-RUN apt-get -y upgrade
-RUN apt-get -y install make gcc patch git unzip bubblewrap curl libgmp-dev bzip2 pkg-config gawk
+# We need to be root to install system dependencies
+USER root
+RUN apt-get update && apt-get install -y gawk git && rm -rf /var/lib/apt/lists/*
+
+# We need to be root to install system dependencies,
+# but opam usually runs as a user. Assuming the base image
+# has a user 'opam', we switch to it.
+USER opam
+WORKDIR /home/opam/iris-tutorial
 
 ARG OPAMYES=true
 ENV OPAMROOTISOK=true
+ARG MODE
 
-RUN curl -sL https://github.com/ocaml/opam/releases/download/2.2.1/opam-2.2.1-x86_64-linux -o opam
-RUN install opam /usr/local/bin/opam
-RUN rm -rf opam
-
-RUN opam init
-RUN eval $(opam env)
-RUN opam repo add --set-default rocq-released https://rocq-prover.org/opam/released
-RUN opam repo add --set-default iris-dev https://gitlab.mpi-sws.org/iris/opam.git
+# 1. Initialize repos
+# With || true in case they already exist in the base image
+RUN opam repo add --set-default rocq-released https://rocq-prover.org/opam/released || true
+RUN opam repo add --set-default iris-dev https://gitlab.mpi-sws.org/iris/opam.git || true
 
-RUN opam switch create stable ocaml.5.2.0
-RUN eval $(opam env)
-RUN opam update
-RUN opam install rocq-core.9.1.1 vsrocq-language-server
-RUN opam install rocq-iris.4.5.0 rocq-iris-heap-lang
+# 2. Copy the opam file from the project root (context is ..)
+COPY --chown=opam:opam iris-tutorial.opam .
 
-RUN opam switch create unstable ocaml.5.2.0
-RUN eval $(opam env)
-RUN opam update
-RUN opam install rocq-core vsrocq-language-server
-RUN opam install rocq-iris rocq-iris-heap-lang rocq-iris-unstable
+# 3. Update and Install dependencies from the .opam file
+RUN opam update && \
+    opam install . --deps-only -y && \
+    opam install -y vsrocq-language-server
 
-RUN opam switch stable
-RUN eval $(opam env)
-RUN opam update
+# 4. If mode is unstable, install the extra unstable package
+RUN if [ "$MODE" = "unstable" ]; then \
+    opam install -y rocq-iris-unstable; \
+    fi
 
-RUN echo 'eval $(opam env)' >> ~/.bashrc
+RUN echo "eval \$(opam env)" >> ~/.bashrc
diff --git a/docker_image/Makefile b/docker_image/Makefile
index 67e387a..5badcd9 100644
--- a/docker_image/Makefile
+++ b/docker_image/Makefile
@@ -1,16 +1,60 @@
+REGISTRY := ghcr.io/logsem/iris-tutorial
+OCAML_VER := 5.5
+MODE ?= stable
+
+# Logic for Base Image and Tags
+ifeq ($(MODE),unstable)
+    BASE_IMAGE := ocaml/opam:debian-unstable-ocaml-5.5
+    IMAGE_NAME := debian-unstable-ocaml-$(OCAML_VER)
+else
+    BASE_IMAGE := ocaml/opam:debian-ocaml-5.5
+    IMAGE_NAME := debian-ocaml-$(OCAML_VER)
+endif
+
 default:
-	@echo 'Please use one of the following targets: x86-64, push-x86-64, arm64, or push-arm64.'
+	@echo 'Usage: make [stable-x86-64 | unstable-x86-64 | stable-arm64 | unstable-arm64]'
+
+# Internal build logic
+build-%:
+	$(eval ARCH_RAW := $*)
+	$(eval PLATFORM := $(if $(filter x86-64,$(ARCH_RAW)),linux/amd64,linux/arm64))
+	$(eval OPAM_ARCH := $(if $(filter x86-64,$(ARCH_RAW)),x86_64-linux,arm64-linux))
+
+	# We use -f to point to the Dockerfile because the context is now ".."
+	docker build \
+		--platform $(PLATFORM) \
+		--build-arg BASE_IMAGE=$(BASE_IMAGE) \
+		--build-arg MODE=$(MODE) \
+		-f Dockerfile \
+		-t $(REGISTRY)/$(IMAGE_NAME)-$(ARCH_RAW) \
+		..
+
+# Public targets
+stable-x86-64:
+	$(MAKE) build-x86-64 MODE=stable
+
+unstable-x86-64:
+	$(MAKE) build-x86-64 MODE=unstable
+
+stable-arm64:
+	$(MAKE) build-arm64 MODE=stable
+
+unstable-arm64:
+	$(MAKE) build-arm64 MODE=unstable
 
-x86-64:
-	docker build --platform linux/amd64 -t ghcr.io/logsem/iris-tutorial/docker-x86-64 .
+# Push targets
+push-stable-x86-64: stable-x86-64
+	docker push $(REGISTRY)/debian-ocaml-$(OCAML_VER)-x86-64
 
-arm64:
-	docker build --platform linux/arm64 -t ghcr.io/logsem/iris-tutorial/docker-arm64 .
+push-unstable-x86-64: unstable-x86-64
+	docker push $(REGISTRY)/debian-unstable-ocaml-$(OCAML_VER)-x86-64
 
-push-x86-64: x86-64
-	docker push ghcr.io/logsem/iris-tutorial/docker-x86-64
+push-stable-arm64: stable-arm64
+	docker push $(REGISTRY)/debian-ocaml-$(OCAML_VER)-arm64
 
-push-arm64: arm64
-	docker push ghcr.io/logsem/iris-tutorial/docker-arm64
+push-unstable-arm64: unstable-arm64
+	docker push $(REGISTRY)/debian-unstable-ocaml-$(OCAML_VER)-arm64
 
-.phony: x86-64 push-x86-64 arm64 push-arm64 default
\ No newline at end of file
+.PHONY: stable-x86-64 unstable-x86-64 stable-arm64 unstable-arm64 \
+	push-stable-x86-64 push-unstable-x86-64 push-stable-arm64 push-unstable-arm64 \
+	default

From 8ee73c7e649b9e11001ab98df39dcf1a12b5d3e3 Mon Sep 17 00:00:00 2001
From: Serhii Khoma <sergey@nordicresults.com>
Date: Thu, 23 Jul 2026 00:40:49 +0700
Subject: [PATCH 7/8] feat: update to latest rocq -> dockerfiles

---
 docker_image/Dockerfile | 25 +++++++++++++++----------
 1 file changed, 15 insertions(+), 10 deletions(-)

diff --git a/docker_image/Dockerfile b/docker_image/Dockerfile
index f832975..2a6b3e8 100644
--- a/docker_image/Dockerfile
+++ b/docker_image/Dockerfile
@@ -3,7 +3,9 @@ FROM ${BASE_IMAGE}
 
 # We need to be root to install system dependencies
 USER root
-RUN apt-get update && apt-get install -y gawk git && rm -rf /var/lib/apt/lists/*
+RUN apt-get update && apt-get install -y \
+    gawk git pkg-config libgmp-dev libmpfr-dev libunwind-dev autoconf \
+    && rm -rf /var/lib/apt/lists/*
 
 # We need to be root to install system dependencies,
 # but opam usually runs as a user. Assuming the base image
@@ -15,18 +17,21 @@ ARG OPAMYES=true
 ENV OPAMROOTISOK=true
 ARG MODE
 
-# 1. Initialize repos
-# With || true in case they already exist in the base image
-RUN opam repo add --set-default rocq-released https://rocq-prover.org/opam/released || true
-RUN opam repo add --set-default iris-dev https://gitlab.mpi-sws.org/iris/opam.git || true
+# 3. Combined Opam Operation
+# This is the "Magic" fix: Adding repos, updating, and installing in ONE step
+# ensures the package solver doesn't use a stale cache.
+RUN opam repo add rocq-released https://rocq-prover.org/opam/released --all --set-default && \
+    opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git --all --set-default && \
+    opam update
 
-# 2. Copy the opam file from the project root (context is ..)
+# TODO: uncomment when vsrocq-language-server will start supporting ocaml 5.5
+# RUN opam install -y -w vsrocq-language-server.2.4.3
+
+# 4. Copy the opam file
 COPY --chown=opam:opam iris-tutorial.opam .
 
-# 3. Update and Install dependencies from the .opam file
-RUN opam update && \
-    opam install . --deps-only -y && \
-    opam install -y vsrocq-language-server
+# 5. Install Project Dependencies
+RUN opam install . --deps-only -y
 
 # 4. If mode is unstable, install the extra unstable package
 RUN if [ "$MODE" = "unstable" ]; then \

From 4bd9798ebf055d2387367458b03eb839b2fa9731 Mon Sep 17 00:00:00 2001
From: Serhii Khoma <sergey@nordicresults.com>
Date: Fri, 24 Jul 2026 10:57:34 +0700
Subject: [PATCH 8/8] feat: update to latest rocq -> to not deal with docker
 images deployments use rocq-prover/docker-opam-action@v1 (replace gawk with
 awk to avoid installing it in ci)

---
 .github/workflows/build.yml | 23 +++++++++--------------
 Makefile                    |  2 +-
 gen-exercises.awk           | 20 ++++++++++++--------
 3 files changed, 22 insertions(+), 23 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index aaa24c7..4fefbc2 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -11,19 +11,14 @@ on:
 jobs:
   build:
     runs-on: ubuntu-latest
-    container:
-      image: ghcr.io/logsem/iris-tutorial/debian-ocaml-5.5-x86-64
-      options: --user opam
-
     steps:
       - uses: actions/checkout@v4
-
-      - name: Build project
-        shell: bash -l {0}
-        run: |
-          # Fix for git ownership issues in containers
-          git config --global --add safe.directory /__w/iris-tutorial/iris-tutorial
-
-          # No need to export HOME=/root, we are opam
-          eval $(opam env)
-          make ci -j2
+      - uses: rocq-prover/docker-opam-action@v1
+        with:
+          rocq_version: '9.1'
+          ocaml_version: '5.5'
+          before_install: |
+            opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git --all --set-default
+          script: |
+            git config --global --add safe.directory "*"
+            make ci -j$(nproc)
diff --git a/Makefile b/Makefile
index 06ade92..2a73763 100644
--- a/Makefile
+++ b/Makefile
@@ -34,7 +34,7 @@ $(EXERCISES): exercises/%.v: theories/%.v gen-exercises.awk
 	  echo "Exercise file $@ has been changed; skipping exercise generation"; \
 	else \
 	  echo "Generating exercise file $@ from $<"; \
-	  gawk -f gen-exercises.awk < $< > $@; \
+	  awk -f gen-exercises.awk < $< > $@; \
 	fi
 
 ci: all
diff --git a/gen-exercises.awk b/gen-exercises.awk
index 895f1e9..0dfd7d6 100644
--- a/gen-exercises.awk
+++ b/gen-exercises.awk
@@ -3,18 +3,22 @@ BEGIN {
     in_auto_solution = 0; # for the simple solution syntax that recognizes `Qed.`
 }
 { # on every line of the input
-    if (match($0, /^( *)\(\* *SOLUTION *\*\) *Proof.$/, groups)) {
-        print groups[1] "Proof."
+    # Capture leading whitespace into 's' to replace groups[1]
+    match($0, /^[ ]*/)
+    s = substr($0, 1, RLENGTH)
+
+    if ($0 ~ /^[ ]*\(\* *SOLUTION *\*\) *Proof.$/) {
+        print s "Proof."
         in_auto_solution = 1
-    } else if (in_auto_solution == 1 && match($0, /^( *)Qed.$/, groups)) {
-        print groups[1] "  (* exercise *)"
-        print groups[1] "Admitted."
+    } else if (in_auto_solution == 1 && $0 ~ /^[ ]*Qed.$/) {
+        print s "  (* exercise *)"
+        print s "Admitted."
         in_auto_solution = 0
-    } else if (match($0, /^( *)\(\* *BEGIN SOLUTION *\*\)$/, groups)) {
+    } else if ($0 ~ /^[ ]*\(\* *BEGIN SOLUTION *\*\)$/) {
         in_solution = 1
-    } else if (match($0, /^( *)\(\* *END SOLUTION BEGIN TEMPLATE *$/, groups)) {
+    } else if ($0 ~ /^[ ]*\(\* *END SOLUTION BEGIN TEMPLATE/) {
         in_solution = 0
-    } else if (match($0, /^( *)END TEMPLATE *\*\)$/, groups)) {
+    } else if ($0 ~ /^[ ]*END TEMPLATE *\*\)$/) {
         # Nothing to do, just do not print this line.
     } else if (in_solution == 0 && in_auto_solution == 0) {
         gsub("From solutions Require", "From exercises Require")