From 135b108ef27b41a732c15c098c9fb6a0c181c154 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Wed, 9 Dec 2020 02:43:59 +0100
Subject: [PATCH] update Coq range to include 8.13 in CI (#24)

* update Coq range to include 8.13 in CI

* explicit hint locality to avoid 8.13 warnings
---
 .github/workflows/{coq-action.yml => docker-ci.yml} | 1 +
 coq-reglang.opam                                    | 2 +-
 meta.yml                                            | 4 +++-
 theories/misc.v                                     | 4 ++--
 4 files changed, 7 insertions(+), 4 deletions(-)
 rename .github/workflows/{coq-action.yml => docker-ci.yml} (94%)

diff --git a/.github/workflows/coq-action.yml b/.github/workflows/docker-ci.yml
similarity index 94%
rename from .github/workflows/coq-action.yml
rename to .github/workflows/docker-ci.yml
index 339a036..aa15eed 100644
--- a/.github/workflows/coq-action.yml
+++ b/.github/workflows/docker-ci.yml
@@ -16,6 +16,7 @@ jobs:
       matrix:
         image:
           - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.13'
           - 'mathcomp/mathcomp:1.12.0-coq-8.12'
           - 'mathcomp/mathcomp:1.11.0-coq-8.12'
           - 'mathcomp/mathcomp:1.10.0-coq-8.11'
diff --git a/coq-reglang.opam b/coq-reglang.opam
index 36290e1..3506c2a 100644
--- a/coq-reglang.opam
+++ b/coq-reglang.opam
@@ -19,7 +19,7 @@ decidability results and closure properties of regular languages."""
 build: [make "-j%{jobs}%" ]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.10" & < "8.13~") | (= "dev")}
+  "coq" {(>= "8.10" & < "8.14~") | (= "dev")}
   "coq-mathcomp-ssreflect" {(>= "1.9" & < "1.13~") | (= "dev")}
 ]
 
diff --git a/meta.yml b/meta.yml
index 63bc2d0..ae6f9c1 100644
--- a/meta.yml
+++ b/meta.yml
@@ -48,7 +48,7 @@ license:
 
 supported_coq_versions:
   text: 8.10 or later (use releases for other Coq versions)
-  opam: '{(>= "8.10" & < "8.13~") | (= "dev")}'
+  opam: '{(>= "8.10" & < "8.14~") | (= "dev")}'
 
 dependencies:
 - opam:
@@ -64,6 +64,8 @@ tested_coq_nix_versions:
 tested_coq_opam_versions:
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
+- version: '1.12.0-coq-8.13'
+  repo: 'mathcomp/mathcomp'
 - version: '1.12.0-coq-8.12'
   repo: 'mathcomp/mathcomp'
 - version: '1.11.0-coq-8.12'
diff --git a/theories/misc.v b/theories/misc.v
index d2954ee..c91dbd8 100644
--- a/theories/misc.v
+++ b/theories/misc.v
@@ -74,7 +74,7 @@ elim: ss => //= s ss IHss.
 by rewrite rev_cons flatten_rcons -IHss rev_cat.
 Qed.
 
-Hint Resolve mem_head : core.
+Global Hint Resolve mem_head : core.
 
 Lemma all1s {T : eqType} {a : T} {s} {P : T -> Prop} :
   (forall b, b \in a :: s -> P b) <-> P a /\ (forall b, b \in s -> P b).
@@ -159,7 +159,7 @@ Definition ord1 {n} := (@Ordinal (n.+2) 1 (erefl _)).
 Lemma inord1 n : ord1 = inord 1 :> 'I_n.+2. 
 Proof. apply: ord_inj => /=. by rewrite inordK. Qed.
 
-Hint Resolve ltn_ord : core.
+Global Hint Resolve ltn_ord : core.
 
 (** Finite Sets - finset.v *)