From 10829a9b042c3647bb907e19b2080cef330c8b28 Mon Sep 17 00:00:00 2001
From: k32 <10274441+k32@users.noreply.github.com>
Date: Fri, 6 Mar 2026 11:02:50 +0100
Subject: [PATCH 1/2] Refactoring: From Coq -> From Stdlib

---
 theories/Storage/Classes.v        | 2 +-
 theories/Storage/Instances/AVL.v  | 2 +-
 theories/Storage/Instances/List.v | 2 +-
 theories/Storage/Properties.v     | 2 +-
 theories/Storage/Tactics.v        | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/Storage/Classes.v b/theories/Storage/Classes.v
index d4de903..a2eacca 100644
--- a/theories/Storage/Classes.v
+++ b/theories/Storage/Classes.v
@@ -1,4 +1,4 @@
-From Coq Require Import
+From Stdlib Require Import
   List
   Classes.EquivDec
   Classes.SetoidClass.
diff --git a/theories/Storage/Instances/AVL.v b/theories/Storage/Instances/AVL.v
index 0edf8fe..4f89fa9 100644
--- a/theories/Storage/Instances/AVL.v
+++ b/theories/Storage/Instances/AVL.v
@@ -1,4 +1,4 @@
-From Coq Require Import
+From Stdlib Require Import
   FMapAVL
   OrderedType
   Classes.EquivDec.
diff --git a/theories/Storage/Instances/List.v b/theories/Storage/Instances/List.v
index 14ae778..5f2cdfb 100644
--- a/theories/Storage/Instances/List.v
+++ b/theories/Storage/Instances/List.v
@@ -1,4 +1,4 @@
-From Coq Require Import
+From Stdlib Require Import
   List
   Classes.EquivDec.
 
diff --git a/theories/Storage/Properties.v b/theories/Storage/Properties.v
index 8acbd3c..ce30750 100644
--- a/theories/Storage/Properties.v
+++ b/theories/Storage/Properties.v
@@ -1,4 +1,4 @@
-From Coq Require Import
+From Stdlib Require Import
   List
   Classes.EquivDec.
 
diff --git a/theories/Storage/Tactics.v b/theories/Storage/Tactics.v
index a789fbc..e8d06b0 100644
--- a/theories/Storage/Tactics.v
+++ b/theories/Storage/Tactics.v
@@ -1,4 +1,4 @@
-From Coq Require Import
+From Stdlib Require Import
   List
   Classes.EquivDec.
 

From 63c911f2aa4eb7fab708088b387a203a5578730e Mon Sep 17 00:00:00 2001
From: k32 <10274441+k32@users.noreply.github.com>
Date: Fri, 6 Mar 2026 11:07:09 +0100
Subject: [PATCH 2/2] CI: bump rocq version

---
 .github/workflows/coqchk.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/coqchk.yml b/.github/workflows/coqchk.yml
index 6c9d934..582dd99 100644
--- a/.github/workflows/coqchk.yml
+++ b/.github/workflows/coqchk.yml
@@ -8,12 +8,12 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - '8.20'
+          - '9.0.1'
         ocaml_version: ['default']
       fail-fast: true  # don't stop jobs if one fails
     steps:
       - uses: actions/checkout@v3
-      - uses: coq-community/docker-coq-action@v1
+      - uses: rocq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-libtx-storage.opam'
           coq_version: ${{ matrix.coq_version }}