Merge pull request #5 from libtx/rocq

Refactoring: From Coq -> From Stdlib

Author: k32

.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 }}

theories/Storage/Classes.v

@@ -1,4 +1,4 @@
-From Coq Require Import
+From Stdlib Require Import
   List
   Classes.EquivDec
   Classes.SetoidClass.

theories/Storage/Instances/AVL.v

@@ -1,4 +1,4 @@
-From Coq Require Import
+From Stdlib Require Import
   FMapAVL
   OrderedType
   Classes.EquivDec.

theories/Storage/Instances/List.v

@@ -1,4 +1,4 @@
-From Coq Require Import
+From Stdlib Require Import
   List
   Classes.EquivDec.
 

theories/Storage/Properties.v

@@ -1,4 +1,4 @@
-From Coq Require Import
+From Stdlib Require Import
   List
   Classes.EquivDec.
 

theories/Storage/Tactics.v

@@ -1,4 +1,4 @@
-From Coq Require Import
+From Stdlib Require Import
   List
   Classes.EquivDec.