From b1e140fb6a4929e1905baebf6fcb9d684ed775e8 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 31 Jan 2024 15:36:06 +0100
Subject: [PATCH] Require Coq >= 8.18

---
 .github/workflows/docker-action.yml |  8 +-------
 README.md                           |  6 +++---
 coq-math-classes.opam               |  2 +-
 meta.yml                            | 12 +++---------
 4 files changed, 8 insertions(+), 20 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 65851c1..2246da3 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -18,14 +18,8 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.19'
           - 'coqorg/coq:8.18'
-          - 'coqorg/coq:8.17'
-          - 'coqorg/coq:8.16'
-          - 'coqorg/coq:8.15'
-          - 'coqorg/coq:8.14'
-          - 'coqorg/coq:8.13'
-          - 'coqorg/coq:8.12'
-          - 'coqorg/coq:8.11'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3
diff --git a/README.md b/README.md
index 9e59e83..fa7bd90 100644
--- a/README.md
+++ b/README.md
@@ -10,8 +10,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![Zulip][zulip-shield]][zulip-link]
 [![DOI][doi-shield]][doi-link]
 
-[docker-action-shield]: https://github.com/coq-community/math-classes/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/coq-community/math-classes/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/math-classes/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/math-classes/actions/workflows/docker-action.yml
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -50,7 +50,7 @@ notations.
 - Coq-community maintainer(s):
   - Bas Spitters ([**@spitters**](https://github.com/spitters))
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: Coq 8.11 or later (use releases for other Coq versions)
+- Compatible Coq versions: Coq 8.18 or later (use releases for other Coq versions)
 - Additional dependencies:
   - [BigNums](https://github.com/coq/bignums)
 - Coq namespace: `MathClasses`
diff --git a/coq-math-classes.opam b/coq-math-classes.opam
index 39c527c..9c5c029 100644
--- a/coq-math-classes.opam
+++ b/coq-math-classes.opam
@@ -30,7 +30,7 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.11" & < "8.19~") | (= "dev")}
+  "coq" {(>= "8.18" & < "8.20~") | (= "dev")}
   "coq-bignums" 
 ]
 
diff --git a/meta.yml b/meta.yml
index 06487b6..bd0d312 100644
--- a/meta.yml
+++ b/meta.yml
@@ -49,19 +49,13 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: Coq 8.11 or later (use releases for other Coq versions)
-  opam: '{(>= "8.11" & < "8.19~") | (= "dev")}'
+  text: Coq 8.18 or later (use releases for other Coq versions)
+  opam: '{(>= "8.18" & < "8.20~") | (= "dev")}'
 
 tested_coq_opam_versions:
 - version: dev
+- version: "8.19"
 - version: "8.18"
-- version: "8.17"
-- version: "8.16"
-- version: "8.15"
-- version: "8.14"
-- version: "8.13"
-- version: "8.12"
-- version: "8.11"
 
 dependencies:
 - opam: