diff --git a/.circleci/config.yml b/.circleci/config.yml
deleted file mode 100644
index 12fd300..0000000
--- a/.circleci/config.yml
+++ /dev/null
@@ -1,90 +0,0 @@
-version: 2.1
-
-jobs:
-  build:
-    parameters:
-      coq:
-        type: string
-    docker:
-    - image: <<parameters.coq>>
-    resource_class: large
-    environment:
-      OPAMJOBS: 4
-      OPAMVERBOSE: 1
-      OPAMYES: true
-      TERM: xterm
-      SKIP_BUILD: |
-        coq-certicoq
-    steps:
-    - checkout
-    - run:
-        name: Pull submodules
-        command: git submodule update --init --recursive
-    - run:
-        name: Configure environment
-        command: echo . ~/.profile >> $BASH_ENV
-    - run:
-        name: Install dependencies
-        command: |
-          opam update
-          opam install --deps-only .
-    - run:
-        name: List installed packages
-        command: opam list
-    - run:
-        name: Build, test, and install package
-        command: opam install -t .
-    - run:
-        name: Generate Coqdoc
-        command: |
-          make -j`nproc` html
-          tar cfz coqdoc.tgz html
-    - store_artifacts:
-        path: coqdoc.tgz
-    - run:
-        name: Test dependants
-        command: |
-          PINS=$(opam list -s --pinned --columns=package | xargs | tr ' ' ,)
-          PACKAGES=`opam list -s --depends-on coq-ext-lib --coinstallable-with $PINS`
-          for PACKAGE in $PACKAGES
-          do DEPS_FAILED=false
-             echo $SKIP_BUILD | tr ' ' '\n' | grep ^$PACKAGE$ > /dev/null &&
-               echo Skip $PACKAGE && continue
-             opam install --deps-only $PACKAGE || DEPS_FAILED=true
-             [ $DEPS_FAILED == true ] || opam install -t $PACKAGE
-          done
-    - run:
-        name: Uninstall package
-        command: opam uninstall .
-
-workflows:
-  version: 2
-  test:
-    jobs:
-    - build:
-        name: "Coq 8.9"
-        coq: "coqorg/coq:8.9"
-    - build:
-        name: "Coq 8.11"
-        coq: "coqorg/coq:8.11"
-    - build:
-        name: "Coq 8.12"
-        coq: "coqorg/coq:8.12"
-    - build:
-        name: "Coq 8.13"
-        coq: "coqorg/coq:8.13"
-    - build:
-        name: "Coq 8.14"
-        coq: "coqorg/coq:8.14"
-    - build:
-        name: "Coq 8.15"
-        coq: "coqorg/coq:8.15"
-    - build:
-        name: "Coq 8.16"
-        coq: "coqorg/coq:8.16"
-    - build:
-        name: "Coq 8.17"
-        coq: "coqorg/coq:8.17"
-    - build:
-        name: "Coq dev"
-        coq: "coqorg/coq:dev"
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
new file mode 100644
index 0000000..3e804ac
--- /dev/null
+++ b/.github/workflows/docker-action.yml
@@ -0,0 +1,72 @@
+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:
+        coq:
+          - '8.9'
+          - '8.11'
+          - '8.12'
+          - '8.13'
+          - '8.14'
+          - '8.15'
+          - '8.16'
+          - '8.17'
+          - 'dev'
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - uses: coq-community/docker-coq-action@v1
+        with:
+          opam_file: 'coq-ext-lib.opam'
+          coq_version: ${{ matrix.coq }}
+          before_script: |
+            startGroup "Workaround permission issue"
+              sudo chown -R coq:coq .
+            endGroup
+          after_script: |
+            set -o pipefail  # recommended if the script uses pipes
+
+            startGroup "Generate Coqdoc"
+              make -j`nproc` html
+            endGroup
+
+            startGroup "Test dependants"
+              opam install conf-clang
+              PINS=$(opam list -s --pinned --columns=package | xargs | tr ' ' ,)
+              PACKAGES=`opam list -s --depends-on coq-ext-lib --coinstallable-with $PINS`
+              for PACKAGE in $PACKAGES
+              do DEPS_FAILED=false
+                 opam install --deps-only $PACKAGE || DEPS_FAILED=true
+                 [ $DEPS_FAILED == true ] || opam install -t $PACKAGE
+              done
+            endGroup
+          export: 'OPAMWITHTEST OPAMCONFIRMLEVEL'
+        env:
+          OPAMWITHTEST: true
+          OPAMCONFIRMLEVEL: unsafe-yes
+      - name: Revert permissions
+        # to avoid a warning at cleanup time
+        if: ${{ always() }}
+        run: sudo chown -R 1001:116 .
+      - uses: actions/upload-artifact@v3
+        with:
+          name: coqdoc
+          path: html
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo
diff --git a/Makefile b/Makefile
index 2a04800..7034571 100644
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,6 @@
 all: theories examples
 
+COQDOCJS_LN?=true
 -include coqdocjs/Makefile.doc
 COQMAKEFILE?=Makefile.coq
 
diff --git a/README.md b/README.md
index c754036..05e650e 100644
--- a/README.md
+++ b/README.md
@@ -4,13 +4,13 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 --->
 # coq-ext-lib
 
-[![CircleCI][circleci-shield]][circleci-link]
+[![Docker CI][docker-action-shield]][docker-action-link]
 [![Contributing][contributing-shield]][contributing-link]
 [![Code of Conduct][conduct-shield]][conduct-link]
 [![Zulip][zulip-shield]][zulip-link]
 
-[circleci-shield]: https://circleci.com/gh/coq-community/coq-ext-lib.svg?style=svg
-[circleci-link]:   https://circleci.com/gh/coq-community/coq-ext-lib
+[docker-action-shield]: https://github.com/coq-community/coq-ext-lib/workflows/Docker%20CI/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/coq-ext-lib/actions?query=workflow:"Docker%20CI"
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
diff --git a/coqdocjs b/coqdocjs
index 556b3ab..5740184 160000
--- a/coqdocjs
+++ b/coqdocjs
@@ -1 +1 @@
-Subproject commit 556b3ab2a3199237cde937fe8ac196cf76099eb8
+Subproject commit 57401849fffb24500c078973a8382dd3086fd2bf
diff --git a/meta.yml b/meta.yml
index 6a334c7..6b05782 100644
--- a/meta.yml
+++ b/meta.yml
@@ -4,7 +4,7 @@ shortname: coq-ext-lib
 opam_name: coq-ext-lib
 organization: coq-community
 community: true
-circleci: false
+action: false
 ci_test_dependants: true
 submodule: true
 
@@ -38,6 +38,8 @@ tested_coq_opam_versions:
   - version: '8.13'
   - version: '8.14'
   - version: '8.15'
+  - version: '8.16'
+  - version: '8.17'
   - version: 'dev'
 
 make_target: theories
@@ -53,6 +55,11 @@ circleci_after_script: |2-
       - store_artifacts:
           path: coqdoc.tgz
 
+action_appendix: |2-
+            export: 'OPAMWITHTEST'
+          env:
+            OPAMWITHTEST: true
+
 documentation: |
   Ideas
   -----
diff --git a/theories/Data/Char.v b/theories/Data/Char.v
index 2930893..53199ba 100644
--- a/theories/Data/Char.v
+++ b/theories/Data/Char.v
@@ -6,7 +6,7 @@ Require Import ExtLib.Core.RelDec.
 Set Implicit Arguments.
 Set Strict Implicit.
 
-Definition ascii_dec (l r : Ascii.ascii) : bool :=
+Definition deprecated_ascii_dec (l r : Ascii.ascii) : bool :=
   match l , r with
     | Ascii.Ascii l1 l2 l3 l4 l5 l6 l7 l8 ,
       Ascii.Ascii r1 r2 r3 r4 r5 r6 r7 r8 =>
@@ -28,7 +28,10 @@ Definition ascii_dec (l r : Ascii.ascii) : bool :=
         else false
   end.
 
-Theorem ascii_dec_sound : forall l r,
+#[deprecated(since="8.9",note="Use Ascii.eqb instead.")]
+Notation ascii_dec := deprecated_ascii_dec.
+
+Theorem deprecated_ascii_dec_sound : forall l r,
   ascii_dec l r = true <-> l = r.
 Proof.
   unfold ascii_dec. intros.
@@ -39,17 +42,20 @@ Proof.
          end; split; congruence.
 Qed.
 
+#[deprecated(since="8.9",note="Use Ascii.eqb_eq instead.")]
+Notation ascii_dec_sound := deprecated_ascii_dec_sound.
+
 Global Instance RelDec_ascii : RelDec (@eq Ascii.ascii) :=
-{ rel_dec := ascii_dec }.
+{ rel_dec := Ascii.eqb }.
 
 Global Instance RelDec_Correct_ascii : RelDec_Correct RelDec_ascii.
 Proof.
-  constructor; auto using ascii_dec_sound.
+  constructor; auto using Ascii.eqb_eq.
 Qed.
 
-Global Instance Reflect_ascii_dec a b : Reflect (ascii_dec a b) (a = b) (a <> b).
+Global Instance Reflect_ascii_dec a b : Reflect (Ascii.eqb a b) (a = b) (a <> b).
 Proof.
-  apply iff_to_reflect; auto using ascii_dec_sound.
+  apply iff_to_reflect; auto using Ascii.eqb_eq.
 Qed.
 
 Definition digit2ascii (n:nat) : Ascii.ascii :=
diff --git a/theories/Data/String.v b/theories/Data/String.v
index 052df91..368df8a 100644
--- a/theories/Data/String.v
+++ b/theories/Data/String.v
@@ -18,9 +18,7 @@ Local Notation "x >> y" := (match x with
                               | z => z
                             end) (only parsing, at level 30).
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since="8.12",note="Use Bool.compare instead.")] *)
-Definition bool_cmp (l r : bool) : comparison :=
+Definition deprecated_bool_cmp (l r : bool) : comparison :=
   match l , r with
     | true , false => Gt
     | false , true => Lt
@@ -28,9 +26,10 @@ Definition bool_cmp (l r : bool) : comparison :=
     | false , false => Eq
   end.
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since="8.15",note="Use Ascii.compare instead.")] *)
-Definition ascii_cmp (l r : Ascii.ascii) : comparison :=
+#[deprecated(since="8.12",note="Use Bool.compare instead.")]
+Notation bool_cmp := deprecated_bool_cmp.
+
+Definition deprecated_ascii_cmp (l r : Ascii.ascii) : comparison :=
   match l , r with
     | Ascii.Ascii l1 l2 l3 l4 l5 l6 l7 l8 ,
       Ascii.Ascii r1 r2 r3 r4 r5 r6 r7 r8 =>
@@ -38,52 +37,58 @@ Definition ascii_cmp (l r : Ascii.ascii) : comparison :=
       bool_cmp l4 r4 >> bool_cmp l3 r3 >> bool_cmp l2 r2 >> bool_cmp l1 r1
   end.
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since="8.9",note="Use String.eqb instead.")] *)
-Fixpoint string_dec (l r : string) : bool :=
+#[deprecated(since="8.15",note="Use Ascii.compare instead.")]
+Notation ascii_cmp := deprecated_ascii_cmp.
+
+Fixpoint deprecated_string_dec (l r : string) : bool :=
   match l , r with
     | EmptyString , EmptyString => true
     | String l ls , String r rs =>
-      if ascii_dec l r then string_dec ls rs
+      if Ascii.eqb l r then deprecated_string_dec ls rs
       else false
     | _ , _ => false
   end.
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since="8.9",note="Use String.eqb_spec instead.")] *)
-Theorem string_dec_sound : forall l r,
+#[deprecated(since="8.9",note="Use String.eqb instead.")]
+Notation string_dec := deprecated_string_dec.
+
+Theorem deprecated_string_dec_sound : forall l r,
   string_dec l r = true <-> l = r.
 Proof.
-  induction l; destruct r; simpl; split; try solve [ intuition ; congruence ];
-  consider (ascii_dec a a0); intros; subst. f_equal. eapply IHl; auto.
-  apply IHl. congruence.
-  inversion H. congruence.
+  induction l; destruct r; try (constructor; easy); simpl.
+  case (Ascii.eqb_spec a a0); simpl; [intros -> | constructor; now intros [= ]].
+  case (IHl r); intros; constructor; intros; f_equal; auto.
+  inversion H1; subst; auto.
 Qed.
 
+#[deprecated(since="8.9",note="Use String.eqb_eq instead.")]
+Notation string_dec_sound := deprecated_string_dec_sound.
+
 Global Instance RelDec_string : RelDec (@eq string) :=
-{| rel_dec := string_dec |}.
+{| rel_dec := String.eqb |}.
 
 Global Instance RelDec_Correct_string : RelDec_Correct RelDec_string.
 Proof.
-  constructor; auto using string_dec_sound.
+  constructor; auto using String.eqb_eq.
 Qed.
 
-Global Instance Reflect_string_dec a b : Reflect (string_dec a b) (a = b) (a <> b).
+Global Instance Reflect_string_dec a b : Reflect (String.eqb a b) (a = b) (a <> b).
 Proof.
-  apply iff_to_reflect; auto using string_dec_sound.
+  apply iff_to_reflect; auto using String.eqb_eq.
 Qed.
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since="8.15",note="Use String.compare instead.")] *)
-Fixpoint string_cmp (l r : string) : comparison :=
+Fixpoint deprecated_string_cmp (l r : string) : comparison :=
   match l , r with
     | EmptyString , EmptyString => Eq
     | EmptyString , _ => Lt
     | _ , EmptyString => Gt
     | String l ls , String r rs =>
-      ascii_cmp l r >> string_cmp ls rs
+      ascii_cmp l r >> deprecated_string_cmp ls rs
   end.
 
+#[deprecated(since="8.15",note="Use String.compare instead.")]
+Notation string_cmp := deprecated_string_cmp.
+
 Section Program_Scope.
   Variable modulus : nat.
   Hypothesis one_lt_mod : 1 < modulus.
diff --git a/theories/Programming/Extras.v b/theories/Programming/Extras.v
index 7bf9c2c..bdfd18f 100644
--- a/theories/Programming/Extras.v
+++ b/theories/Programming/Extras.v
@@ -23,22 +23,27 @@ Module FunNotation.
 End FunNotation.
 Import FunNotation.
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since = "8.13", note = "Use standard library.")] *)
-Definition uncurry A B C (f:A -> B -> C) (x:A * B) : C := let (a,b) := x in f a b.
+Definition deprecated_uncurry A B C (f:A -> B -> C) (x:A * B) : C := let (a,b) := x in f a b.
 
-(* Uncomment the following line after we drop Coq 8.8: *)
-(* #[deprecated(since = "8.13", note = "Use standard library.")] *)
-Definition curry  {A B C} (f : A * B -> C) (a : A) (b : B) : C := f (a, b).
+#[deprecated(since = "8.13", note = "Use standard library.")]
+Notation uncurry := deprecated_uncurry.
 
-Lemma uncurry_curry : forall A B C (f : A -> B -> C) a b,
+Definition deprecated_curry  {A B C} (f : A * B -> C) (a : A) (b : B) : C := f (a, b).
+
+#[deprecated(since = "8.13", note = "Use standard library.")]
+Notation curry := deprecated_curry.
+
+Lemma deprecated_uncurry_curry : forall A B C (f : A -> B -> C) a b,
     curry (uncurry f) a b = f a b.
 Proof.
   unfold curry, uncurry.
   reflexivity.
 Qed.
 
-Lemma curry_uncurry : forall A B C (f : A * B -> C) ab,
+#[deprecated(since = "8.13", note = "Use standard library.")]
+Notation uncurry_curry := deprecated_uncurry_curry.
+
+Lemma deprecated_curry_uncurry : forall A B C (f : A * B -> C) ab,
     uncurry (curry f) ab = f ab.
 Proof.
   unfold uncurry, curry.
@@ -46,20 +51,29 @@ Proof.
   reflexivity.
 Qed.
 
-Fixpoint zip A B (xs:list A) (ys:list B) : list (A * B) :=
+#[deprecated(since = "8.13", note = "Use standard library.")]
+Notation curry_uncurry := deprecated_curry_uncurry.
+
+Fixpoint deprecated_zip A B (xs:list A) (ys:list B) : list (A * B) :=
   match xs, ys with
   | [], _ => []
   | _, [] => []
-  | x::xs, y::ys => (x,y)::zip xs ys
+  | x::xs, y::ys => (x,y)::deprecated_zip xs ys
   end
 .
 
-Fixpoint unzip A B (xys:list (A * B)) : list A * list B :=
+#[deprecated(note = "Use List.combine instead.")]
+Notation zip := deprecated_zip.
+
+Fixpoint deprecated_unzip A B (xys:list (A * B)) : list A * list B :=
 match xys with
 | [] => ([], [])
-| (x,y)::xys => let (xs,ys) := unzip xys in (x::xs,y::ys)
+| (x,y)::xys => let (xs,ys) := deprecated_unzip xys in (x::xs,y::ys)
 end.
 
+#[deprecated(note = "Use List.split instead.")]
+Notation unzip := deprecated_unzip.
+
 Definition sum_tot {A} (x:A + A) : A := match x with inl a => a | inr a => a end.
 
 Definition forEach A B (xs:list A) (f:A -> B) : list B := map f xs.