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 → .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'

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")}
 ]
 

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'

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 *)