Merge pull request #44 Update boilerplate for MathComp 1.14.0

Author: chdoc

.github/workflows/docker-action.yml

@@ -20,6 +20,8 @@ jobs:
       matrix:
         image:
           - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.14'
           - 'mathcomp/mathcomp:1.13.0-coq-8.15'
           - 'mathcomp/mathcomp:1.13.0-coq-8.14'
           - 'mathcomp/mathcomp:1.13.0-coq-8.13'

coq-reglang.opam

@@ -20,7 +20,7 @@ build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "2.5"}
   "coq" {(>= "8.10" & < "8.16~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.11" & < "1.14~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.11" & < "1.15~") | (= "dev")}
 ]
 
 tags: [

meta.yml

@@ -54,7 +54,7 @@ supported_coq_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "1.11" & < "1.14~") | (= "dev")}'
+    version: '{(>= "1.11" & < "1.15~") | (= "dev")}'
   description: |-
     [MathComp](https://math-comp.github.io) 1.11.0 or later (`ssreflect` suffices)
 
@@ -69,6 +69,10 @@ tested_coq_nix_versions:
 tested_coq_opam_versions:
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
+- version: '1.14.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
+- version: '1.14.0-coq-8.14'
+  repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.14'

theories/languages.v

@@ -91,7 +91,7 @@ Definition plus l1 l2 : dlang char := [pred w | (w \in l1) || (w \in l2)].
 Definition residual x l : dlang char := [pred w | x :: w \in l].
 
 (** For the concatenation of two decidable languages, we use finite
-types. Note that we need to use [L1] and [L2] applicatively in order
+types. Note that we need to use [l1] and [l2] applicatively in order
 for the termination check for [star] to succeed. *)
 
 Definition conc l1 l2 : dlang char :=