diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
deleted file mode 100644
index 43c321c..0000000
--- a/.github/workflows/coq-action.yml
+++ /dev/null
@@ -1,38 +0,0 @@
-name: CI
-
-on:
-  push:
-    branches:
-      - master
-  pull_request:
-    branches:
-      - '**'
-
-jobs:
-  build:
-    # the OS must be GNU/Linux to be able to use the docker-coq-action
-    runs-on: ubuntu-latest
-    strategy:
-      matrix:
-        image:
-          - 'mathcomp/mathcomp:1.11.0-coq-8.10'
-          - 'mathcomp/mathcomp:1.11.0-coq-8.11'
-          - 'mathcomp/mathcomp:1.11.0-coq-8.12'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.10'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.11'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.12'
-          - 'mathcomp/mathcomp-dev:coq-8.10'
-          - 'mathcomp/mathcomp-dev:coq-8.11'
-          - 'mathcomp/mathcomp-dev:coq-8.12'
-          - 'mathcomp/mathcomp-dev:coq-dev'
-      fail-fast: false
-    steps:
-      - uses: actions/checkout@v2
-      - uses: coq-community/docker-coq-action@v1
-        with:
-          opam_file: 'coq-mathcomp-finmap.opam'
-          custom_image: ${{ matrix.image }}
-
-# See also:
-# https://github.com/coq-community/docker-coq-action#readme
-# https://github.com/erikmd/docker-coq-github-action-demo
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
new file mode 100644
index 0000000..3bf41d6
--- /dev/null
+++ b/.github/workflows/docker-action.yml
@@ -0,0 +1,53 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+name: Docker CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'mathcomp/mathcomp:1.11.0-coq-8.11'
+          - 'mathcomp/mathcomp:1.11.0-coq-8.12'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.11'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.12'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.13'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.11'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.12'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.13'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.11'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.12'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.13'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.14.0-coq-dev'
+          - 'mathcomp/mathcomp-dev:coq-8.11'
+          - 'mathcomp/mathcomp-dev:coq-8.12'
+          - 'mathcomp/mathcomp-dev:coq-8.13'
+          - 'mathcomp/mathcomp-dev:coq-8.14'
+          - 'mathcomp/mathcomp-dev:coq-8.15'
+          - 'mathcomp/mathcomp-dev:coq-dev'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v2
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-mathcomp-finmap.opam'
+          custom_image: ${{ matrix.image }}
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo
diff --git a/README.md b/README.md
index aca1ed6..44f71c5 100644
--- a/README.md
+++ b/README.md
@@ -1,9 +1,13 @@
+<!---
+This file was generated from `meta.yml`, please do not edit manually.
+Follow the instructions on https://github.com/coq-community/templates to regenerate.
+--->
 # Finite maps
 
-[![CI][action-shield]][action-link]
+[![Docker CI][docker-action-shield]][docker-action-link]
 
-[action-shield]: https://github.com/math-comp/finmap/workflows/CI/badge.svg?branch=master
-[action-link]: https://github.com/math-comp/finmap/actions?query=workflow%3ACI
+[docker-action-shield]: https://github.com/math-comp/finmap/workflows/Docker%20CI/badge.svg?branch=master
+[docker-action-link]: https://github.com/math-comp/finmap/actions?query=workflow:"Docker%20CI"
 
 
 
@@ -20,10 +24,9 @@ which will be used to subsume notations for finite sets, eventually.
   - Cyril Cohen (initial)
   - Kazuhiko Sakaguchi
 - License: [CeCILL-B](CECILL-B)
-- Compatible Coq versions: Coq 8.10 to 8.12
+- Compatible Coq versions: Coq 8.11 to 8.15
 - Additional dependencies:
-  - [MathComp ssreflect 1.10 to 1.12](https://math-comp.github.io)
-  - [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough)
+  - [MathComp ssreflect 1.11 to 1.14](https://math-comp.github.io)
 - Coq namespace: `mathcomp.finmap`
 - Related publication(s): none
 
diff --git a/coq-mathcomp-finmap.opam b/coq-mathcomp-finmap.opam
index cc8a618..7d2e5f9 100644
--- a/coq-mathcomp-finmap.opam
+++ b/coq-mathcomp-finmap.opam
@@ -1,3 +1,6 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
 opam-version: "2.0"
 maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
 version: "dev"
@@ -15,12 +18,11 @@ types). This includes support for functions with finite support and
 multisets. The library also contains a generic order and set libary,
 which will be used to subsume notations for finite sets, eventually."""
 
-build: [make "-j%{jobs}%" ]
+build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.10" & < "8.13~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.13~") | (= "dev") }
-  "coq-mathcomp-bigenough" {>= "1.0.0"}
+  "coq" { (>= "8.11" & < "8.16~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "1.11.0" & < "1.15~") | (= "dev") }
 ]
 
 tags: [
diff --git a/finmap.v b/finmap.v
index d06e8e5..2aa32bd 100644
--- a/finmap.v
+++ b/finmap.v
@@ -354,7 +354,7 @@ Reserved Notation "\bigcup_ ( i 'in' A ) F"
 
 Reserved Notation "{fmap T }" (at level 0, format "{fmap  T }").
 Reserved Notation "x .[ k <- v ]"
-  (at level 2, k at level 200, v at level 200, format "x .[ k  <-  v ]").
+  (at level 2, left associativity, format "x .[ k  <-  v ]").
 Reserved Notation "x .[~ k ]" (at level 2, k at level 200, format "x .[~  k ]").
 Reserved Notation "x .[& k ]" (at level 2, k at level 200, format "x .[&  k ]").
 Reserved Notation "x .[\ k ]" (at level 2, k at level 200, format "x .[\  k ]").
@@ -1202,7 +1202,7 @@ Implicit Types (a b x : K) (A B C D : {fset K}) (E : {fset K'})
 Lemma fsetP {A B} : A =i B <-> A = B.
 Proof. by split=> [eqAB|-> //]; apply/val_inj/canonical_eq_keys => //= a. Qed.
 
-CoInductive in_fset_spec (A : {fset K}) (x : K) : K -> bool -> Prop :=
+Variant in_fset_spec (A : {fset K}) (x : K) : K -> bool -> Prop :=
  | InFset (u : A) & x = val u : in_fset_spec A x (val u) true
  | OutFset of x \notin A : in_fset_spec A x x false.
 
@@ -2954,6 +2954,8 @@ Notation "x .[ k <- v ]" := (setf x k v) : fmap_scope.
 Notation "f .[? k ]" := (fnd f k) : fmap_scope.
 
 Section FinMapCanonicals.
+
+Section FinMapEncode.
 Variable K : choiceType.
 
 Let finMap_on (V : Type) (d : {fset K}) := {ffun d -> V}.
@@ -2964,22 +2966,32 @@ Definition finMap_decode V (f : finMap_ V) := FinMap (tagged f).
 Lemma finMap_codeK V : cancel (@finMap_encode V) (@finMap_decode V).
 Proof. by case. Qed.
 
+End FinMapEncode.
+
 Section FinMapEqType.
-Variable V : eqType.
+Variable (K : choiceType) (V : eqType).
 
-Definition finMap_eqMixin := CanEqMixin (@finMap_codeK V).
+Definition finMap_eqMixin := CanEqMixin (@finMap_codeK K V).
 Canonical finMap_eqType := EqType {fmap K -> V} finMap_eqMixin.
 
 End FinMapEqType.
 
 Section FinMapChoiceType.
-Variable V : choiceType.
+Variable (K V : choiceType).
 
-Definition finMap_choiceMixin := CanChoiceMixin (@finMap_codeK V).
+Definition finMap_choiceMixin := CanChoiceMixin (@finMap_codeK K V).
 Canonical finMap_choiceType := ChoiceType {fmap K -> V} finMap_choiceMixin.
 
 End FinMapChoiceType.
 
+Section FinMapCountType.
+Variable (K V : countType).
+
+Definition finMap_countMixin := CanCountMixin (@finMap_codeK K V).
+Canonical finMap_countType := CountType {fmap K -> V} finMap_countMixin.
+
+End FinMapCountType.
+
 End FinMapCanonicals.
 
 Section FinMapTheory.
@@ -3640,7 +3652,7 @@ Proof. by rewrite mem_finsupp negbK. Qed.
 Lemma fsfun_dflt f k : k \notin finsupp f -> f k = default k.
 Proof. by rewrite mem_finsupp negbK => /eqP. Qed.
 
-CoInductive fsfun_spec f k : V -> bool -> Type :=
+Variant fsfun_spec f k : V -> bool -> Type :=
   | FsfunOut : k \notin finsupp f -> fsfun_spec f k (default k) false
   | FsfunIn  (kf : k \in finsupp f) : fsfun_spec f k (f k) true.
 
@@ -3754,6 +3766,11 @@ Definition fsfun_choiceMixin (K V : choiceType) (d : K -> V) :=
 Canonical  fsfun_choiceType (K V : choiceType) (d : K -> V) :=
   ChoiceType (fsfun d) (fsfun_choiceMixin d).
 
+Definition fsfun_countMixin (K V : countType) (d : K -> V) :=
+  [countMixin of fsfun d by <:].
+Canonical  fsfun_countType (K V : countType) (d : K -> V) :=
+  CountType (fsfun d) (fsfun_countMixin d).
+
 Declare Scope fsfun_scope.
 Delimit Scope fsfun_scope with fsfun.
 
diff --git a/meta.yml b/meta.yml
index 8897b6a..1fabd3e 100644
--- a/meta.yml
+++ b/meta.yml
@@ -31,42 +31,64 @@ license:
   file: CECILL-B
 
 supported_coq_versions:
-  text: Coq 8.10 to 8.12
-  opam: '{ (>= "8.10" & < "8.13~") | (= "dev") }'
+  text: Coq 8.11 to 8.15
+  opam: '{ (>= "8.11" & < "8.16~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '1.11.0-coq-8.10'
-  repo: 'mathcomp/mathcomp'
 - version: '1.11.0-coq-8.11'
   repo: 'mathcomp/mathcomp'
 - version: '1.11.0-coq-8.12'
   repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.10'
-  repo: 'mathcomp/mathcomp'
 - version: '1.12.0-coq-8.11'
   repo: 'mathcomp/mathcomp'
 - version: '1.12.0-coq-8.12'
   repo: 'mathcomp/mathcomp'
-- version: 'coq-8.10'
-  repo: 'mathcomp/mathcomp-dev'
+- version: '1.12.0-coq-8.13'
+  repo: 'mathcomp/mathcomp'
+- version: '1.12.0-coq-8.14'
+  repo: 'mathcomp/mathcomp'
+- version: '1.13.0-coq-8.11'
+  repo: 'mathcomp/mathcomp'
+- version: '1.13.0-coq-8.12'
+  repo: 'mathcomp/mathcomp'
+- version: '1.13.0-coq-8.13'
+  repo: 'mathcomp/mathcomp'
+- version: '1.13.0-coq-8.14'
+  repo: 'mathcomp/mathcomp'
+- version: '1.13.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
+- version: '1.14.0-coq-8.11'
+  repo: 'mathcomp/mathcomp'
+- version: '1.14.0-coq-8.12'
+  repo: 'mathcomp/mathcomp'
+- version: '1.14.0-coq-8.13'
+  repo: 'mathcomp/mathcomp'
+- version: '1.14.0-coq-8.14'
+  repo: 'mathcomp/mathcomp'
+- version: '1.14.0-coq-8.15'
+  repo: 'mathcomp/mathcomp'
+- version: '1.14.0-coq-dev'
+  repo: 'mathcomp/mathcomp'
 - version: 'coq-8.11'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.12'
   repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-8.13'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-8.14'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-8.15'
+  repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "1.11.0" & < "1.13~") | (= "dev") }'
+    version: '{ (>= "1.11.0" & < "1.15~") | (= "dev") }'
   description: |-
-    [MathComp ssreflect 1.10 to 1.12](https://math-comp.github.io)
-- opam:
-    name: coq-mathcomp-bigenough
-    version: '{>= "1.0.0"}'
-  description: |-
-    [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough)
+    [MathComp ssreflect 1.11 to 1.14](https://math-comp.github.io)
+
 namespace: mathcomp.finmap
 
 keywords:
diff --git a/opam-release.sh b/opam-release.sh
new file mode 100755
index 0000000..78937d5
--- /dev/null
+++ b/opam-release.sh
@@ -0,0 +1,60 @@
+#!/usr/bin/env bash
+set -e
+# set -x
+
+if [ -z $1 ] || [ -z $2 ] || [ -z $3 ] || [ -z $4 ] || \
+   [ $1 == "--help" ] || [ $1 == "-h" ]
+then cat <<EOF
+usage : packager GITHUBUSER PROJECT VERSION URL"
+- GITHUBUSER is your github username, you must have a fork of
+    coq/opam-coq-archive under
+    https://github.com/$GITHUBUSER/opam-coq-archive
+    for this command to work
+- VERSION is the opam version number of the package to create
+- PROJECT is a name of the project, without space, it is used
+    solely for generating the name of the branch and PR
+- URL is the url of the archive associated with the version to
+    release
+EOF
+     exit 0
+else
+GITHUBUSER=$1
+PROJECT=$2
+VERSION=$3
+URL=$4
+fi
+
+COA=$(mktemp -d) # stands for Coq Opam Archive
+git clone --depth=10 git@github.com:coq/opam-coq-archive $COA -o upstream
+git -C $COA remote add\
+  origin git@github.com:$GITHUBUSER/opam-coq-archive
+BRANCH=$PROJECT.$VERSION
+git -C $COA checkout -b $BRANCH
+PKGS=$COA/released/packages
+
+ARCHIVE=$(mktemp)
+curl -L $URL -o $ARCHIVE
+SUM=$(sha256sum $ARCHIVE | cut -d " " -f 1)
+
+for opam in *.opam
+do B=$(basename $opam .opam)
+   P=$PKGS/$B/$B.$VERSION
+   mkdir -p $P
+   sed "/^version:.*/d" $opam > $P/opam
+   echo "" >> $P/opam
+   echo "url {" >> $P/opam
+   echo "  src: \"$URL\"" >> $P/opam
+   echo "  checksum: \"sha256=$SUM\"" >> $P/opam
+   echo "}" >> $P/opam
+
+   opam lint --check-upstream $P/opam
+
+   git -C $COA add $P/opam
+done
+git -C $COA commit -m "Release $PROJECT $VERSION"
+git -C $COA push origin -f $BRANCH
+
+echo "**********************************************************************"
+echo "Create a pull request by visiting"
+echo "https://github.com/$GITHUBUSER/opam-coq-archive/pull/new/$BRANCH"
+echo "**********************************************************************"