Fix

.github/workflows/docker-action.yml

@@ -29,13 +29,17 @@ jobs:
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.2.0-coq-8.20'
           - 'mathcomp/mathcomp:2.2.0-coq-dev'
-          - 'mathcomp/mathcomp-dev:coq-8.18'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.3.0-coq-8.20'
+          - 'mathcomp/mathcomp:2.3.0-coq-dev'
           - 'mathcomp/mathcomp-dev:coq-8.19'
           - 'mathcomp/mathcomp-dev:coq-8.20'
-          - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp-dev:rocq-prover-9.0'
+          - 'mathcomp/mathcomp-dev:rocq-prover-dev'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-lemma-overloading.opam'

meta.yml

@@ -81,13 +81,21 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-dev'
   repo: 'mathcomp/mathcomp'
-- version: 'coq-8.18'
-  repo: 'mathcomp/mathcomp-dev'
+- version: '2.3.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
+- version: '2.3.0-coq-8.19'
+  repo: 'mathcomp/mathcomp'
+- version: '2.3.0-coq-8.20'
+  repo: 'mathcomp/mathcomp'
+- version: '2.3.0-coq-dev'
+  repo: 'mathcomp/mathcomp'
 - version: 'coq-8.19'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.20'
   repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-dev'
+- version: 'rocq-prover-9.0'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'rocq-prover-dev'
   repo: 'mathcomp/mathcomp-dev'
 
 dependencies:

resources/index.md

@@ -1,4 +1,6 @@
 ---
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
 title: Lemma Overloading
 lang: en
 header-includes:
@@ -10,9 +12,9 @@ header-includes:
     <style type="text/css"> body { width: 1100px; margin-left: 30px; }</style>
 ---
 
-<div style="text-align:left"><img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px">
-[View the project on GitHub](https://github.com/coq-community/lemma-overloading)
-<img src="https://github.githubassets.com/images/modules/logos_page/Octocat.png" height="25" style="border:0px"></div>
+<div style="text-align:left"><img src="https://gist.github.com/johan/1007813/raw/a25829510f049194b6404a8f98d22978e8744a6f/octocat.svg" height="25" style="border:0px">
+<a href="https://github.com/coq-community/lemma-overloading">View the project on GitHub</a>
+<img src="https://gist.github.com/johan/1007813/raw/a25829510f049194b6404a8f98d22978e8744a6f/octocat.svg" height="25" style="border:0px"></div>
 
 ## About
 
@@ -53,7 +55,10 @@ Other related publications, if any, are listed below.
 
 ## Authors and contributors
 
-- Georges Gonthier
-- Beta Ziliani
-- Aleksandar Nanevski
-- Derek Dreyer
+- Georges Gonthier (initial)
+- Beta Ziliani (initial)
+- Aleksandar Nanevski (initial)
+- Derek Dreyer (initial)
+
+
+

theories/ordtype.v

@@ -16,7 +16,8 @@
 *)
 
 From HB Require Import structures.
-From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq fintype.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
+From mathcomp Require Import fintype.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.