From 92e8d7dec9be9d838a9a16a22fd189faa93391f8 Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Thu, 28 Apr 2022 23:53:09 +0200
Subject: [PATCH] bump lower coq limit

---
 .github/workflows/docker-action.yml | 2 +-
 README.md                           | 4 ++--
 coq-fcsl-pcm.opam                   | 2 +-
 meta.yml                            | 8 ++++----
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 8776a03..1799f8e 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -17,7 +17,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.13.0-coq-8.13'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
           - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false
diff --git a/README.md b/README.md
index 459833f..1567d4a 100644
--- a/README.md
+++ b/README.md
@@ -27,9 +27,9 @@ This library relies on propositional and functional extentionality axioms.
 - Author(s):
   - Aleksandar Nanevski (initial)
 - License: [Apache-2.0](LICENSE)
-- Compatible Coq versions: Coq 8.13 to 8.15
+- Compatible Coq versions: Coq 8.14 to 8.15
 - Additional dependencies:
-  - [MathComp ssreflect 1.13 to 1.15](https://math-comp.github.io)
+  - [MathComp ssreflect 1.13 to 1.14](https://math-comp.github.io)
 - Coq namespace: `fcsl`
 - Related publication(s): none
 
diff --git a/coq-fcsl-pcm.opam b/coq-fcsl-pcm.opam
index a937778..98502a0 100644
--- a/coq-fcsl-pcm.opam
+++ b/coq-fcsl-pcm.opam
@@ -25,7 +25,7 @@ This library relies on propositional and functional extentionality axioms."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.13" & < "8.16~") | (= "dev") }
+  "coq" { (>= "8.14" & < "8.16~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.15~") | (= "dev") }
 ]
 
diff --git a/meta.yml b/meta.yml
index 55734af..70473c4 100644
--- a/meta.yml
+++ b/meta.yml
@@ -36,11 +36,11 @@ license:
   file: LICENSE
 
 supported_coq_versions:
-  text: Coq 8.13 to 8.15
-  opam: '{ (>= "8.13" & < "8.16~") | (= "dev") }'
+  text: Coq 8.14 to 8.15
+  opam: '{ (>= "8.14" & < "8.16~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '1.13.0-coq-8.13'
+- version: '1.13.0-coq-8.14'
   repo: 'mathcomp/mathcomp'
 - version: '1.14.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
@@ -52,7 +52,7 @@ dependencies:
     name: coq-mathcomp-ssreflect
     version: '{ (>= "1.13.0" & < "1.15~") | (= "dev") }'
   description: |-
-    [MathComp ssreflect 1.13 to 1.15](https://math-comp.github.io)
+    [MathComp ssreflect 1.13 to 1.14](https://math-comp.github.io)
 
 namespace: fcsl