From 7bce55da6438e255fb27e1d8ac9ef2c82f7032a1 Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Tue, 29 Dec 2020 19:33:36 -0500
Subject: [PATCH 01/43] meta: standard licence identifier

---
 README.md        | 8 ++++++--
 coq-ext-lib.opam | 2 +-
 meta.yml         | 4 ++--
 3 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/README.md b/README.md
index 1fe3370c..6d3c861d 100644
--- a/README.md
+++ b/README.md
@@ -1,3 +1,7 @@
+<!---
+This file was generated from `meta.yml`, please do not edit manually.
+Follow the instructions on https://github.com/coq-community/templates to regenerate.
+--->
 # coq-ext-lib
 
 [![CircleCI][circleci-shield]][circleci-link]
@@ -28,7 +32,7 @@ A collection of theories and plugins that may be useful in other Coq development
 - Coq-community maintainer(s):
   - Gregory Malecha ([**@gmalecha**](https://github.com/gmalecha))
   - Yishuai Li ([**@liyishuai**](https://github.com/liyishuai))
-- License: [The FreeBSD Copyright](LICENSE)
+- License: [BSD 2-Clause FreeBSD License](LICENSE)
 - Compatible Coq versions: Coq 8.8 or later
 - Additional dependencies: none
 - Coq namespace: `ExtLib`
@@ -47,7 +51,7 @@ opam install coq-ext-lib
 To instead build and install manually, do:
 
 ``` shell
-git clone https://github.com/coq-community/coq-ext-lib.git
+git clone --recurse-submodules https://github.com/coq-community/coq-ext-lib.git
 cd coq-ext-lib
 make theories  # or make -j <number-of-cores-on-your-machine> theories
 make install
diff --git a/coq-ext-lib.opam b/coq-ext-lib.opam
index 07ef44a0..d2922fe3 100644
--- a/coq-ext-lib.opam
+++ b/coq-ext-lib.opam
@@ -4,7 +4,7 @@ homepage: "https://github.com/coq-community/coq-ext-lib"
 dev-repo: "git+https://github.com/coq-community/coq-ext-lib.git"
 bug-reports: "https://github.com/coq-community/coq-ext-lib/issues"
 authors: ["Gregory Malecha"]
-license: "BSD"
+license: "BSD-2-Clause-FreeBSD"
 build: [
   [make "-j%{jobs}%" "theories"]
 ]
diff --git a/meta.yml b/meta.yml
index f5dd5daa..c7e2f135 100644
--- a/meta.yml
+++ b/meta.yml
@@ -25,8 +25,8 @@ maintainers:
 opam-file-maintainer: "gmalecha@gmail.com"
 
 license:
-  fullname: The FreeBSD Copyright
-  identifier: BSD
+  fullname: BSD 2-Clause FreeBSD License
+  identifier: BSD-2-Clause-FreeBSD
 
 supported_coq_versions:
   text: Coq 8.8 or later

From 737425e3f2d92820a7d0045c421f59c282cac861 Mon Sep 17 00:00:00 2001
From: jadephilipoom <jadep@google.com>
Date: Thu, 28 Jan 2021 18:36:19 +0000
Subject: [PATCH 02/43] Make Monad_stateT a local instance (#106)

---
 examples/StateTMonad.v            | 15 +++++++++++++++
 examples/_CoqProject              |  3 ++-
 theories/Data/Monads/StateMonad.v |  6 ++++--
 3 files changed, 21 insertions(+), 3 deletions(-)
 create mode 100644 examples/StateTMonad.v

diff --git a/examples/StateTMonad.v b/examples/StateTMonad.v
new file mode 100644
index 00000000..fb8081a2
--- /dev/null
+++ b/examples/StateTMonad.v
@@ -0,0 +1,15 @@
+From ExtLib Require Import
+     Monad
+     OptionMonad
+     StateMonad.
+
+(** [Monad_stateT] is not in context, so this definition fails *)
+Fail Definition foo : stateT unit option unit :=
+  ret tt.
+
+(** Use [Existing Instance] to bring the Local [Monad_stateT] instance into context *)
+Existing Instance Monad_stateT.
+
+(** Now the definition succeeds *)
+Definition foo : stateT unit option unit :=
+  ret tt.
diff --git a/examples/_CoqProject b/examples/_CoqProject
index 4998808e..f6ed9c07 100644
--- a/examples/_CoqProject
+++ b/examples/_CoqProject
@@ -7,4 +7,5 @@ MonadReasoning.v
 Printing.v
 UsingSets.v
 WithDemo.v
-Notations.v
\ No newline at end of file
+Notations.v
+StateTMonad.v
diff --git a/theories/Data/Monads/StateMonad.v b/theories/Data/Monads/StateMonad.v
index af50696a..24485848 100644
--- a/theories/Data/Monads/StateMonad.v
+++ b/theories/Data/Monads/StateMonad.v
@@ -43,8 +43,10 @@ Section StateType.
   Definition execStateT {t} (c : stateT t) (s : S) : m S :=
     bind (runStateT c s) (fun x => ret (snd x)).
 
-
-  Global Instance Monad_stateT : Monad stateT :=
+  (** [Monad_stateT] is not a Global Instance because it can cause an infinite loop
+     in typeclass inference under certain circumstances. Use [Existing Instance
+     Monad_stateT.] to bring the instance into context. *)
+  Instance Monad_stateT : Monad stateT :=
   { ret := fun _ x => mkStateT (fun s => @ret _ M _ (x,s))
   ; bind := fun _ _ c1 c2 =>
     mkStateT (fun s =>

From c3e301b39599626079fd2ff2c4244011ae57ac66 Mon Sep 17 00:00:00 2001
From: Li-yao Xia <lysxia@gmail.com>
Date: Sun, 7 Mar 2021 13:10:15 -0500
Subject: [PATCH 03/43] Monad: Remove dependency on id and flip

---
 theories/Structures/Monad.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/theories/Structures/Monad.v b/theories/Structures/Monad.v
index bab11714..4647cdec 100644
--- a/theories/Structures/Monad.v
+++ b/theories/Structures/Monad.v
@@ -1,6 +1,3 @@
-From Coq Require Import
-     Basics.
-Require Import ExtLib.Core.Any.
 Require Import ExtLib.Structures.Functor.
 Require Import ExtLib.Structures.Applicative.
 
@@ -49,7 +46,8 @@ Section monadic.
              (f: T -> m U) (g: U -> m V): (T -> m V) :=
     fun x => bind (f x) g.
 
-  Definition join {m a} `{Monad m} : m (m a) -> m a := flip bind id.
+  Definition join@{d c} {m : Type@{d} -> Type@{c}} {a} `{Monad m} : m (m a) -> m a :=
+    fun x => bind x (fun y => y).
 
 End monadic.
 

From 7532d92d1d6a9d7c9c45e111766f65421f6e09ba Mon Sep 17 00:00:00 2001
From: Li-yao Xia <lysxia@gmail.com>
Date: Sun, 14 Mar 2021 16:52:20 -0400
Subject: [PATCH 04/43] Monad: Allow patterns in 'let*' notation

---
 theories/Structures/Monad.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Structures/Monad.v b/theories/Structures/Monad.v
index 4647cdec..2b500330 100644
--- a/theories/Structures/Monad.v
+++ b/theories/Structures/Monad.v
@@ -81,8 +81,8 @@ Module MonadLetNotation.
 
   Export MonadBaseNotation.
 
-  Notation "'let*' x ':=' c1 'in' c2" := (@bind _ _ _ _ c1 (fun x => c2))
-    (at level 61, c1 at next level, right associativity) : monad_scope.
+  Notation "'let*' p ':=' c1 'in' c2" := (@bind _ _ _ _ c1 (fun p => c2))
+    (at level 61, p as pattern, c1 at next level, right associativity) : monad_scope.
 
 End MonadLetNotation.
 

From 2cc43de5dc303f973531a64720e2cf9cfe2fb071 Mon Sep 17 00:00:00 2001
From: Andrej Dudenhefner <mrhaandi@gmail.com>
Date: Wed, 24 Mar 2021 11:55:29 +0100
Subject: [PATCH 05/43] fix coq PR 13986

---
 theories/Data/ListNth.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/Data/ListNth.v b/theories/Data/ListNth.v
index 4c05df36..de2502e4 100644
--- a/theories/Data/ListNth.v
+++ b/theories/Data/ListNth.v
@@ -1,4 +1,5 @@
 Require Import Coq.Lists.List.
+Require Import Coq.Arith.Lt Coq.Arith.Plus.
 
 Set Implicit Arguments.
 Set Strict Implicit.

From 6ff2bdb069b7d34f2f429ce594b08fe327502770 Mon Sep 17 00:00:00 2001
From: Jim Fehrle <jim.fehrle@gmail.com>
Date: Sat, 27 Mar 2021 22:25:18 -0700
Subject: [PATCH 06/43] Replace use of omega with lia for Coq 8.14 #13741

---
 examples/ConsiderDemo.v         |  5 +++--
 theories/Data/ListFirstnSkipn.v | 37 +++++++++++++++++----------------
 2 files changed, 22 insertions(+), 20 deletions(-)

diff --git a/examples/ConsiderDemo.v b/examples/ConsiderDemo.v
index ef9f98d7..20c1f404 100644
--- a/examples/ConsiderDemo.v
+++ b/examples/ConsiderDemo.v
@@ -5,6 +5,7 @@ Require Import ExtLib.Tactics.Consider.
 Require Import ExtLib.Data.Nat.
 
 Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -15,7 +16,7 @@ Section test.
                  ltb x z = true.
   intros x y z.
   consider (ltb x y && ltb y z).
-  consider (ltb x z); auto. intros. exfalso. omega.
+  consider (ltb x z); auto. intros. exfalso. lia.
   Qed.
 
   Goal forall x y z,
@@ -24,7 +25,7 @@ Section test.
     ltb x z = true.
   Proof.
     intros. consider (ltb x y); consider (ltb y z); consider (ltb x z); intros; auto.
-    exfalso; omega.
+    exfalso; lia.
   Qed.
 
 End test.
diff --git a/theories/Data/ListFirstnSkipn.v b/theories/Data/ListFirstnSkipn.v
index 4bd3321d..ad5e284c 100644
--- a/theories/Data/ListFirstnSkipn.v
+++ b/theories/Data/ListFirstnSkipn.v
@@ -1,13 +1,14 @@
 Require Import Coq.Lists.List.
 Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
 
 Lemma firstn_app_L : forall T n (a b : list T),
   n <= length a ->
   firstn n (a ++ b) = firstn n a.
 Proof.
   induction n; destruct a; simpl in *; intros; auto.
-  exfalso; omega.
-  f_equal. eapply IHn; eauto. omega.
+  exfalso; lia.
+  f_equal. eapply IHn; eauto. lia.
 Qed.
 
 Lemma firstn_app_R : forall T n (a b : list T),
@@ -15,8 +16,8 @@ Lemma firstn_app_R : forall T n (a b : list T),
   firstn n (a ++ b) = a ++ firstn (n - length a) b.
 Proof.
   induction n; destruct a; simpl in *; intros; auto.
-  exfalso; omega.
-  f_equal. eapply IHn; eauto. omega.
+  exfalso; lia.
+  f_equal. eapply IHn; eauto. lia.
 Qed.
 
 Lemma firstn_all : forall T n (a : list T),
@@ -24,8 +25,8 @@ Lemma firstn_all : forall T n (a : list T),
   firstn n a = a.
 Proof.
   induction n; destruct a; simpl; intros; auto.
-  exfalso; omega.
-  simpl. f_equal. eapply IHn; omega.
+  exfalso; lia.
+  simpl. f_equal. eapply IHn; lia.
 Qed.
 
 Lemma firstn_0 : forall T n (a : list T),
@@ -40,19 +41,19 @@ Lemma firstn_cons : forall T n a (b : list T),
   firstn n (a :: b) = a :: firstn (n - 1) b.
 Proof.
   destruct n; intros.
-  omega.
-  simpl. replace (n - 0) with n; [ | omega ]. reflexivity.
+  lia.
+  simpl. replace (n - 0) with n; [ | lia ]. reflexivity.
 Qed.
 
-Hint Rewrite firstn_app_L firstn_app_R firstn_all firstn_0 firstn_cons using omega : list_rw.
+Hint Rewrite firstn_app_L firstn_app_R firstn_all firstn_0 firstn_cons using lia : list_rw.
 
 Lemma skipn_app_R : forall T n (a b : list T),
   length a <= n ->
   skipn n (a ++ b) = skipn (n - length a) b.
 Proof.
   induction n; destruct a; simpl in *; intros; auto.
-  exfalso; omega.
-  eapply IHn. omega.
+  exfalso; lia.
+  eapply IHn. lia.
 Qed.
 
 Lemma skipn_app_L : forall T n (a b : list T),
@@ -60,8 +61,8 @@ Lemma skipn_app_L : forall T n (a b : list T),
   skipn n (a ++ b) = (skipn n a) ++ b.
 Proof.
   induction n; destruct a; simpl in *; intros; auto.
-  exfalso; omega.
-  eapply IHn. omega.
+  exfalso; lia.
+  eapply IHn. lia.
 Qed.
 
 Lemma skipn_0 : forall T n (a : list T),
@@ -76,8 +77,8 @@ Lemma skipn_all : forall T n (a : list T),
   skipn n a = nil.
 Proof.
   induction n; destruct a; simpl in *; intros; auto.
-  exfalso; omega.
-  apply IHn; omega.
+  exfalso; lia.
+  apply IHn; lia.
 Qed.
 
 Lemma skipn_cons : forall T n a (b : list T),
@@ -85,8 +86,8 @@ Lemma skipn_cons : forall T n a (b : list T),
   skipn n (a :: b) = skipn (n - 1) b.
 Proof.
   destruct n; intros.
-  omega.
-  simpl. replace (n - 0) with n; [ | omega ]. reflexivity.
+  lia.
+  simpl. replace (n - 0) with n; [ | lia ]. reflexivity.
 Qed.
 
-Hint Rewrite skipn_app_L skipn_app_R skipn_0 skipn_all skipn_cons using omega : list_rw.
+Hint Rewrite skipn_app_L skipn_app_R skipn_0 skipn_all skipn_cons using lia : list_rw.

From 1549e74c4356c2e324b435930e8377b92a8e17b2 Mon Sep 17 00:00:00 2001
From: Yishuai Li <liyishuai@users.noreply.github.com>
Date: Thu, 1 Apr 2021 01:34:16 -0400
Subject: [PATCH 07/43] Switch license to BSD-2-Clause

since FreeBSD is deprecated by SPDX
---
 LICENSE          | 9 ++++-----
 README.md        | 2 +-
 coq-ext-lib.opam | 2 +-
 meta.yml         | 4 ++--
 4 files changed, 8 insertions(+), 9 deletions(-)

diff --git a/LICENSE b/LICENSE
index 41d325a4..3ac855e5 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,3 +1,5 @@
+BSD 2-Clause License
+
 Copyright (c) 2013, Gregory M. Malecha
 All rights reserved.
 
@@ -6,6 +8,7 @@ modification, are permitted provided that the following conditions are met:
 
 1. Redistributions of source code must retain the above copyright notice, this
    list of conditions and the following disclaimer. 
+
 2. Redistributions in binary form must reproduce the above copyright notice,
    this list of conditions and the following disclaimer in the documentation
    and/or other materials provided with the distribution. 
@@ -13,14 +16,10 @@ modification, are permitted provided that the following conditions are met:
 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
 ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
-DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
 ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-
-The views and conclusions contained in the software and documentation are those
-of the authors and should not be interpreted as representing official policies, 
-either expressed or implied, of the FreeBSD Project.
\ No newline at end of file
diff --git a/README.md b/README.md
index 6d3c861d..fbc05265 100644
--- a/README.md
+++ b/README.md
@@ -32,7 +32,7 @@ A collection of theories and plugins that may be useful in other Coq development
 - Coq-community maintainer(s):
   - Gregory Malecha ([**@gmalecha**](https://github.com/gmalecha))
   - Yishuai Li ([**@liyishuai**](https://github.com/liyishuai))
-- License: [BSD 2-Clause FreeBSD License](LICENSE)
+- License: [BSD 2-Clause "Simplified" License](LICENSE)
 - Compatible Coq versions: Coq 8.8 or later
 - Additional dependencies: none
 - Coq namespace: `ExtLib`
diff --git a/coq-ext-lib.opam b/coq-ext-lib.opam
index d2922fe3..6f5abadd 100644
--- a/coq-ext-lib.opam
+++ b/coq-ext-lib.opam
@@ -4,7 +4,7 @@ homepage: "https://github.com/coq-community/coq-ext-lib"
 dev-repo: "git+https://github.com/coq-community/coq-ext-lib.git"
 bug-reports: "https://github.com/coq-community/coq-ext-lib/issues"
 authors: ["Gregory Malecha"]
-license: "BSD-2-Clause-FreeBSD"
+license: "BSD-2-Clause"
 build: [
   [make "-j%{jobs}%" "theories"]
 ]
diff --git a/meta.yml b/meta.yml
index c7e2f135..f4dd8905 100644
--- a/meta.yml
+++ b/meta.yml
@@ -25,8 +25,8 @@ maintainers:
 opam-file-maintainer: "gmalecha@gmail.com"
 
 license:
-  fullname: BSD 2-Clause FreeBSD License
-  identifier: BSD-2-Clause-FreeBSD
+  fullname: BSD 2-Clause "Simplified" License
+  identifier: BSD-2-Clause
 
 supported_coq_versions:
   text: Coq 8.8 or later

From 968fb49a1f1044adf87f8e427cbe2d83d525d37d Mon Sep 17 00:00:00 2001
From: Yishuai Li <liyishuai@users.noreply.github.com>
Date: Sun, 2 May 2021 14:36:04 -0400
Subject: [PATCH 08/43]  MonadExc instance for option (#112)

* CircleCI generated from template

* CI update OCaml

* MonadExc instance for option
---
 .circleci/config.yml               | 19 +++++++++++--------
 meta.yml                           | 18 ++++++++++++++----
 theories/Data/Monads/OptionMonad.v |  8 ++++++++
 3 files changed, 33 insertions(+), 12 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 8005e94f..6723b66f 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -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.
+
 version: 2.1
 
 jobs:
@@ -66,14 +69,14 @@ workflows:
         name: "Coq 8.10"
         coq: "coqorg/coq:8.10"
     - build:
-        name: "Coq 8.11"
-        coq: "coqorg/coq:8.11"
+        name: "Coq 8.11-ocaml-4.11-flambda"
+        coq: "coqorg/coq:8.11-ocaml-4.11-flambda"
     - build:
-        name: "Coq 8.12"
-        coq: "coqorg/coq:8.12"
+        name: "Coq 8.12-ocaml-4.11-flambda"
+        coq: "coqorg/coq:8.12-ocaml-4.11-flambda"
     - build:
-        name: "Coq 8.13"
-        coq: "coqorg/coq:8.13"
+        name: "Coq 8.13-ocaml-4.11-flambda"
+        coq: "coqorg/coq:8.13-ocaml-4.11-flambda"
     - build:
-        name: "Coq dev"
-        coq: "coqorg/coq:dev"
+        name: "Coq dev-ocaml-4.11-flambda"
+        coq: "coqorg/coq:dev-ocaml-4.11-flambda"
diff --git a/meta.yml b/meta.yml
index f4dd8905..43247d50 100644
--- a/meta.yml
+++ b/meta.yml
@@ -36,14 +36,24 @@ tested_coq_opam_versions:
   - version: '8.8'
   - version: '8.9'
   - version: '8.10'
-  - version: '8.11'
-  - version: '8.12'
-  - version: '8.13'
-  - version: 'dev'
+  - version: '8.11-ocaml-4.11-flambda'
+  - version: '8.12-ocaml-4.11-flambda'
+  - version: '8.13-ocaml-4.11-flambda'
+  - version: 'dev-ocaml-4.11-flambda'
 
 make_target: theories
+test_target: examples
 namespace: ExtLib
 
+circleci_after_script: |2-
+      - run:
+          name: Generate Coqdoc
+          command: |
+            make -j`nproc` html
+            tar cfz coqdoc.tgz html
+      - store_artifacts:
+          path: coqdoc.tgz
+
 documentation: |
   Ideas
   -----
diff --git a/theories/Data/Monads/OptionMonad.v b/theories/Data/Monads/OptionMonad.v
index bc07b40f..752b4f43 100644
--- a/theories/Data/Monads/OptionMonad.v
+++ b/theories/Data/Monads/OptionMonad.v
@@ -25,6 +25,14 @@ Global Instance Plus_option : MonadPlus option :=
     end
 }.
 
+Global Instance Exception_option : MonadExc unit option :=
+{ raise _ _   := None
+; catch _ c h := match c with
+                 | None   => h tt
+                 | Some x => Some x
+                 end
+}.
+
 Section Trans.
   Variable m : Type -> Type.
 

From 73fa2d83a075adedc65c1f5888d7f688f9e31f0c Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Thu, 2 Sep 2021 00:27:35 -0400
Subject: [PATCH 09/43] ListMonad: use flat_map from stdlib

---
 theories/Data/Monads/ListMonad.v | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/theories/Data/Monads/ListMonad.v b/theories/Data/Monads/ListMonad.v
index dfdd2e85..a3cc69c6 100644
--- a/theories/Data/Monads/ListMonad.v
+++ b/theories/Data/Monads/ListMonad.v
@@ -6,11 +6,7 @@ Set Strict Implicit.
 
 Global Instance Monad_list : Monad list :=
 { ret := fun _ v => v :: nil
-; bind := fun _ _ => fix recur c1 c2 :=
-  match c1 with
-    | nil => nil
-    | a :: b => c2 a ++ recur b c2
-  end
+; bind := fun _ _ l f => flat_map f l
 }.
 
 Global Instance MonadZero_list : MonadZero list :=

From 6ab8408b94204c2174a66b548eb4bc8c7eaefbc7 Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Mon, 13 Sep 2021 17:14:33 -0400
Subject: [PATCH 10/43] String: prefer stdlib

---
 theories/Data/String.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/theories/Data/String.v b/theories/Data/String.v
index 7d4b32c1..052df919 100644
--- a/theories/Data/String.v
+++ b/theories/Data/String.v
@@ -18,6 +18,8 @@ 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 :=
   match l , r with
     | true , false => Gt
@@ -26,6 +28,8 @@ 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 :=
   match l , r with
     | Ascii.Ascii l1 l2 l3 l4 l5 l6 l7 l8 ,
@@ -34,6 +38,8 @@ 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 :=
   match l , r with
     | EmptyString , EmptyString => true
@@ -43,6 +49,8 @@ Fixpoint string_dec (l r : string) : bool :=
     | _ , _ => 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,
   string_dec l r = true <-> l = r.
 Proof.
@@ -65,6 +73,8 @@ Proof.
   apply iff_to_reflect; auto using string_dec_sound.
 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 :=
   match l , r with
     | EmptyString , EmptyString => Eq

From 162c470fc1060152f21c098728c8ac9d4a012637 Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Tue, 21 Sep 2021 14:52:05 -0400
Subject: [PATCH 11/43] FMapAList: add alternative definition

---
 theories/Data/Map/FMapAList.v | 38 ++++++++++++++++++++++++++++++++++-
 1 file changed, 37 insertions(+), 1 deletion(-)

diff --git a/theories/Data/Map/FMapAList.v b/theories/Data/Map/FMapAList.v
index c0f1fabd..72b2f152 100644
--- a/theories/Data/Map/FMapAList.v
+++ b/theories/Data/Map/FMapAList.v
@@ -6,6 +6,15 @@ Require Import ExtLib.Structures.Maps.
 Require Import ExtLib.Structures.Monad.
 Require Import ExtLib.Structures.Reducible.
 Require Import ExtLib.Structures.Functor.
+From Coq Require Import
+     Basics.
+From ExtLib Require Import
+     Extras
+     OptionMonad.
+Import
+  FunNotation
+  FunctorNotation.
+Open Scope program_scope.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -35,6 +44,20 @@ Section keyed.
           alist_find k ms
     end.
 
+  Definition alist_find' (k: K) : alist -> option V :=
+    fmap snd ∘ find (rel_dec k ∘ fst).
+
+  Lemma alist_find_alt (m: alist) : forall k: K,
+      alist_find k m = alist_find' k m.
+  Proof.
+    induction m; intuition.
+    unfold alist_find', compose.
+    simpl.
+    destruct (k ?[ R ] a0) eqn:Heq; intuition.
+    rewrite IHm.
+    reflexivity.
+  Qed.
+
   Section fold.
     Import MonadNotation.
     Local Open Scope monad_scope.
@@ -49,6 +72,19 @@ Section keyed.
           let acc := f k v acc in
           fold_alist acc m
       end.
+
+    Definition fold_alist' : T -> alist -> T :=
+      flip $ fold_left (flip $ uncurry f).
+
+    Lemma fold_alist_alt (map: alist) : forall acc: T,
+        fold_alist acc map = fold_alist' acc map.
+    Proof.
+      induction map; intuition.
+      simpl.
+      rewrite IHmap.
+      reflexivity.
+    Qed.
+
   End fold.
 
   Definition alist_union (m1 m2 : alist) : alist :=
@@ -208,4 +244,4 @@ Module TEST.
         | S n => find_all n
       end) 500.
 End TEST.
-*)
\ No newline at end of file
+*)

From aeb71ca2f5e5538f23f287772d3d84b35241415a Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Thu, 23 Sep 2021 00:56:21 -0400
Subject: [PATCH 12/43] CI for Coq 8.14

---
 .circleci/config.yml | 3 +++
 meta.yml             | 1 +
 2 files changed, 4 insertions(+)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 6723b66f..b5459b6b 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -77,6 +77,9 @@ workflows:
     - build:
         name: "Coq 8.13-ocaml-4.11-flambda"
         coq: "coqorg/coq:8.13-ocaml-4.11-flambda"
+    - build:
+        name: "Coq 8.14-ocaml-4.12-flambda"
+        coq: "coqorg/coq:8.14-ocaml-4.12-flambda"
     - build:
         name: "Coq dev-ocaml-4.11-flambda"
         coq: "coqorg/coq:dev-ocaml-4.11-flambda"
diff --git a/meta.yml b/meta.yml
index 43247d50..702edcca 100644
--- a/meta.yml
+++ b/meta.yml
@@ -39,6 +39,7 @@ tested_coq_opam_versions:
   - version: '8.11-ocaml-4.11-flambda'
   - version: '8.12-ocaml-4.11-flambda'
   - version: '8.13-ocaml-4.11-flambda'
+  - version: '8.14-ocaml-4.12-flambda'
   - version: 'dev-ocaml-4.11-flambda'
 
 make_target: theories

From 6fdc35861007436701841d375cb37c32ba658f53 Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Sun, 26 Sep 2021 22:32:51 -0400
Subject: [PATCH 13/43] MonadLaws: add back return_of_bind

---
 theories/Structures/MonadLaws.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/Structures/MonadLaws.v b/theories/Structures/MonadLaws.v
index 44b068e4..a95e10fd 100644
--- a/theories/Structures/MonadLaws.v
+++ b/theories/Structures/MonadLaws.v
@@ -22,6 +22,8 @@ Section MonadLaws.
   Class MonadLaws :=
   { bind_of_return : forall {A B} (a : A) (f : A -> m B),
       bind (ret a) f = f a
+  ; return_of_bind : forall {A} (aM: m A),
+      bind aM ret = aM
   ; bind_associativity :
       forall {A B C} (aM:m A) (f:A -> m B) (g:B -> m C),
         bind (bind aM f) g = bind aM (fun a => bind (f a) g)

From 92470dd5a27715c29fd0b72efd0231762c70eafc Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Mon, 4 Oct 2021 23:48:35 -0400
Subject: [PATCH 14/43] Generate index with old template

---
 .gitignore  | 1 +
 .gitmodules | 3 +++
 Makefile    | 2 +-
 meta.yml    | 2 ++
 templates   | 1 +
 5 files changed, 8 insertions(+), 1 deletion(-)
 create mode 160000 templates

diff --git a/.gitignore b/.gitignore
index d760dcfd..d422fbe7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -19,6 +19,7 @@ deps.pdf
 .DS_Store
 html
 index.md
+index.html
 *.coq.d
 *.vok
 *.vos
diff --git a/.gitmodules b/.gitmodules
index 849a6b35..61c12847 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,3 +1,6 @@
 [submodule "coqdocjs"]
 	path = coqdocjs
 	url = https://github.com/coq-community/coqdocjs.git
+[submodule "templates"]
+	path = templates
+	url = https://github.com/coq-community/templates.git
diff --git a/Makefile b/Makefile
index 2e7ece93..59a70081 100644
--- a/Makefile
+++ b/Makefile
@@ -28,7 +28,7 @@ dist:
 
 .PHONY: all clean dist theories examples html
 
-TEMPLATES ?= ../templates
+TEMPLATES ?= templates
 
 index.html: index.md
 	pandoc -s $^ -o $@
diff --git a/meta.yml b/meta.yml
index 702edcca..60cb2c72 100644
--- a/meta.yml
+++ b/meta.yml
@@ -77,6 +77,8 @@ documentation: |
     - Base directory to the provided theories
 
 coqdoc_index: |
+  - [0.11.4](v0.11.4/toc.html)
+  - [0.11.3](v0.11.3/toc.html)
   - [0.11.2](v0.11.2/toc.html)
   - [0.11.1](v0.11.1/toc.html)
   - [0.11.0](v0.11.0/toc.html)
diff --git a/templates b/templates
new file mode 160000
index 00000000..36b28e03
--- /dev/null
+++ b/templates
@@ -0,0 +1 @@
+Subproject commit 36b28e037139db4c684e6ad2e1eb72bf92ede393

From 43e979ba74200ec924c28561b3f189fe37ff5c07 Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Tue, 5 Oct 2021 00:17:02 -0400
Subject: [PATCH 15/43] CI from new template

---
 .circleci/config.yml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index b5459b6b..29571f77 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -48,9 +48,11 @@ jobs:
         command: |
           PINS=$(opam list -s --pinned --columns=package | xargs | tr ' ' ,)
           PACKAGES=`opam list -s --depends-on coq-ext-lib --coinstallable-with $PINS`
-          if [ -n "$PACKAGES" ]
-          then opam install -t $PACKAGES
-          fi
+          for PACKAGE in $PACKAGES
+          do DEPS_FAILED=false
+             opam install --deps-only $PACKAGE || DEPS_FAILED=true
+             [ $DEPS_FAILED == true ] || opam install -t $PACKAGE
+          done
     - run:
         name: Uninstall package
         command: opam uninstall .

From 8f0f0228332007a1b73abb01fb9bf828023007fa Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Fri, 29 Oct 2021 16:10:28 -0400
Subject: [PATCH 16/43] v0.11.5 documentation

---
 meta.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/meta.yml b/meta.yml
index 60cb2c72..c65108cb 100644
--- a/meta.yml
+++ b/meta.yml
@@ -77,6 +77,7 @@ documentation: |
     - Base directory to the provided theories
 
 coqdoc_index: |
+  - [0.11.5](v0.11.5/toc.html)
   - [0.11.4](v0.11.4/toc.html)
   - [0.11.3](v0.11.3/toc.html)
   - [0.11.2](v0.11.2/toc.html)

From ca0795cd59d64940fd386c45df800296532eb23d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Thu, 6 Jan 2022 18:42:09 +0100
Subject: [PATCH 17/43] Adapt w.r.t. coq/coq#15442.

---
 theories/Programming/Show.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Programming/Show.v b/theories/Programming/Show.v
index 76807b6e..4203fe7d 100644
--- a/theories/Programming/Show.v
+++ b/theories/Programming/Show.v
@@ -177,7 +177,7 @@ Section hiding_notation.
   Next Obligation.
     assert (NPeano.Nat.div n 10 < n) ; eauto.
     eapply NPeano.Nat.div_lt.
-    inversion H; apply Lt.lt_O_Sn.
+    match goal with [ H : n > _ |- _ ] => inversion H end; apply Lt.lt_O_Sn.
     repeat constructor.
   Defined.
   Global Instance nat_Show : Show nat := { show := nat_show }.

From ea8a8622d839f3251d12dbbef84f36e1c78c9421 Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Tue, 18 Jan 2022 13:32:15 -0500
Subject: [PATCH 18/43] CI for Coq 8.15

---
 .circleci/config.yml | 4 +++-
 meta.yml             | 2 +-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 29571f77..54e08072 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -27,7 +27,6 @@ jobs:
     - run:
         name: Install dependencies
         command: |
-          opam repo -a --set-default add coq-extra-dev https://coq.inria.fr/opam/extra-dev
           opam update
           opam install --deps-only .
     - run:
@@ -82,6 +81,9 @@ workflows:
     - build:
         name: "Coq 8.14-ocaml-4.12-flambda"
         coq: "coqorg/coq:8.14-ocaml-4.12-flambda"
+    - build:
+        name: "Coq 8.15-ocaml-4.12-flambda"
+        coq: "coqorg/coq:8.15-ocaml-4.12-flambda"
     - build:
         name: "Coq dev-ocaml-4.11-flambda"
         coq: "coqorg/coq:dev-ocaml-4.11-flambda"
diff --git a/meta.yml b/meta.yml
index c65108cb..e89831ca 100644
--- a/meta.yml
+++ b/meta.yml
@@ -6,7 +6,6 @@ organization: coq-community
 community: true
 circleci: true
 ci_test_dependants: true
-ci_extra_dev: true
 submodule: true
 
 synopsis: A library of Coq definitions, theorems, and tactics
@@ -40,6 +39,7 @@ tested_coq_opam_versions:
   - version: '8.12-ocaml-4.11-flambda'
   - version: '8.13-ocaml-4.11-flambda'
   - version: '8.14-ocaml-4.12-flambda'
+  - version: '8.15-ocaml-4.12-flambda'
   - version: 'dev-ocaml-4.11-flambda'
 
 make_target: theories

From 99f7abd16ae7e611f7b92051fbdea4254de44d82 Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Wed, 12 Jan 2022 16:19:37 -0500
Subject: [PATCH 19/43] Move Data.Monads.ListMonad to Data.List

---
 _CoqProject                      |  1 -
 theories/Data/List.v             | 11 +++++++++--
 theories/Data/Monads/ListMonad.v | 17 -----------------
 3 files changed, 9 insertions(+), 20 deletions(-)
 delete mode 100644 theories/Data/Monads/ListMonad.v

diff --git a/_CoqProject b/_CoqProject
index 5aa5e542..5930a73a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -119,7 +119,6 @@ theories/Data/Monads/FuelMonadLaws.v
 theories/Data/Monads/FuelMonad.v
 theories/Data/Monads/IdentityMonadLaws.v
 theories/Data/Monads/IdentityMonad.v
-theories/Data/Monads/ListMonad.v
 theories/Data/Monads/OptionMonadLaws.v
 theories/Data/Monads/OptionMonad.v
 theories/Data/Monads/ReaderMonadLaws.v
diff --git a/theories/Data/List.v b/theories/Data/List.v
index 03e4fabe..4de1f73c 100644
--- a/theories/Data/List.v
+++ b/theories/Data/List.v
@@ -98,7 +98,7 @@ Global Instance Foldable_list@{u} {T : Type@{u}} : Foldable (list T) T :=
 
 Require Import ExtLib.Structures.Traversable.
 Require Import ExtLib.Structures.Functor.
-Require Import ExtLib.Structures.Monad.
+Require Import ExtLib.Structures.Monads.
 Require Import ExtLib.Structures.Applicative.
 
 Section traversable.
@@ -123,7 +123,14 @@ Monomorphic Universe listU.
 Global Instance Monad_list@{} : Monad@{listU listU} list :=
 { ret  := fun _ x => x :: nil
 ; bind := fun _ _ x f =>
-  List.fold_right (fun x acc => f x ++ acc) nil x
+  flat_map f x
+}.
+
+Global Instance MonadZero_list : MonadZero list :=
+{ mzero := @nil }.
+
+Global Instance MonadPlus_list : MonadPlus list :=
+{ mplus _A _B a b := List.map inl a ++ List.map inr b
 }.
 
 Section list.
diff --git a/theories/Data/Monads/ListMonad.v b/theories/Data/Monads/ListMonad.v
deleted file mode 100644
index a3cc69c6..00000000
--- a/theories/Data/Monads/ListMonad.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import ExtLib.Structures.Monads.
-Require Import List.
-
-Set Implicit Arguments.
-Set Strict Implicit.
-
-Global Instance Monad_list : Monad list :=
-{ ret := fun _ v => v :: nil
-; bind := fun _ _ l f => flat_map f l
-}.
-
-Global Instance MonadZero_list : MonadZero list :=
-{ mzero := @nil }.
-
-Global Instance MonadPlus_list : MonadPlus list :=
-{ mplus _A _B a b := List.map inl a ++ List.map inr b
-}.

From 4d87b5a93fa7aaf77428a5d7818ed7ba56809dce Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Wed, 19 Jan 2022 06:50:35 -0500
Subject: [PATCH 20/43] v0.11.6 documentation

---
 meta.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/meta.yml b/meta.yml
index e89831ca..6c1a1365 100644
--- a/meta.yml
+++ b/meta.yml
@@ -77,6 +77,7 @@ documentation: |
     - Base directory to the provided theories
 
 coqdoc_index: |
+  - [0.11.6](v0.11.6/toc.html)
   - [0.11.5](v0.11.5/toc.html)
   - [0.11.4](v0.11.4/toc.html)
   - [0.11.3](v0.11.3/toc.html)

From 8fa1a3c681c53c25070fcf022daeab6d27dc3151 Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Wed, 19 Jan 2022 14:03:15 -0500
Subject: [PATCH 21/43] Publish script

---
 Makefile | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Makefile b/Makefile
index 59a70081..2a04800c 100644
--- a/Makefile
+++ b/Makefile
@@ -35,3 +35,7 @@ index.html: index.md
 
 index.md: meta.yml
 	$(TEMPLATES)/generate.sh $@
+
+publish%:
+	opam publish --packages-directory=released/packages \
+		--repo=coq/opam-coq-archive --tag=v$* -v $* coq-community/coq-ext-lib

From 506d2985cc540ad7b4a788d9a20f6ec57e75a510 Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Sun, 5 Jun 2022 22:33:40 -0400
Subject: [PATCH 22/43] Update Docker tag

---
 .circleci/config.yml | 12 ++++++------
 meta.yml             |  4 ++--
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 54e08072..f6b83502 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -10,9 +10,9 @@ jobs:
         type: string
     docker:
     - image: <<parameters.coq>>
-    resource_class: medium
+    resource_class: large
     environment:
-      OPAMJOBS: 2
+      OPAMJOBS: 4
       OPAMVERBOSE: 1
       OPAMYES: true
       TERM: xterm
@@ -76,8 +76,8 @@ workflows:
         name: "Coq 8.12-ocaml-4.11-flambda"
         coq: "coqorg/coq:8.12-ocaml-4.11-flambda"
     - build:
-        name: "Coq 8.13-ocaml-4.11-flambda"
-        coq: "coqorg/coq:8.13-ocaml-4.11-flambda"
+        name: "Coq 8.13-ocaml-4.12-flambda"
+        coq: "coqorg/coq:8.13-ocaml-4.12-flambda"
     - build:
         name: "Coq 8.14-ocaml-4.12-flambda"
         coq: "coqorg/coq:8.14-ocaml-4.12-flambda"
@@ -85,5 +85,5 @@ workflows:
         name: "Coq 8.15-ocaml-4.12-flambda"
         coq: "coqorg/coq:8.15-ocaml-4.12-flambda"
     - build:
-        name: "Coq dev-ocaml-4.11-flambda"
-        coq: "coqorg/coq:dev-ocaml-4.11-flambda"
+        name: "Coq dev-ocaml-4.12-flambda"
+        coq: "coqorg/coq:dev-ocaml-4.12-flambda"
diff --git a/meta.yml b/meta.yml
index 6c1a1365..13a49e04 100644
--- a/meta.yml
+++ b/meta.yml
@@ -37,10 +37,10 @@ tested_coq_opam_versions:
   - version: '8.10'
   - version: '8.11-ocaml-4.11-flambda'
   - version: '8.12-ocaml-4.11-flambda'
-  - version: '8.13-ocaml-4.11-flambda'
+  - version: '8.13-ocaml-4.12-flambda'
   - version: '8.14-ocaml-4.12-flambda'
   - version: '8.15-ocaml-4.12-flambda'
-  - version: 'dev-ocaml-4.11-flambda'
+  - version: 'dev-ocaml-4.12-flambda'
 
 make_target: theories
 test_target: examples

From 756c36c2633891b9d185e75077e2b1579b0a638a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Wed, 29 Jun 2022 11:05:52 +0200
Subject: [PATCH 23/43] Adapt w.r.t. coq/coq#16004.

---
 examples/StateTMonad.v           | 2 +-
 theories/Core/Any.v              | 1 +
 theories/Data/Eq.v               | 8 ++++++++
 theories/Data/ListFirstnSkipn.v  | 5 +++++
 theories/Data/Option.v           | 4 ++++
 theories/Data/PList.v            | 1 +
 theories/Data/POption.v          | 2 ++
 theories/Data/SigT.v             | 4 ++++
 theories/Generic/Ind.v           | 2 ++
 theories/Programming/Eqv.v       | 1 +
 theories/Programming/Injection.v | 3 +++
 theories/Programming/Le.v        | 3 +++
 theories/Tactics/BoolTac.v       | 6 +++++-
 theories/Tactics/Consider.v      | 1 +
 14 files changed, 41 insertions(+), 2 deletions(-)

diff --git a/examples/StateTMonad.v b/examples/StateTMonad.v
index fb8081a2..11b905b1 100644
--- a/examples/StateTMonad.v
+++ b/examples/StateTMonad.v
@@ -8,7 +8,7 @@ Fail Definition foo : stateT unit option unit :=
   ret tt.
 
 (** Use [Existing Instance] to bring the Local [Monad_stateT] instance into context *)
-Existing Instance Monad_stateT.
+#[global] Existing Instance Monad_stateT.
 
 (** Now the definition succeeds *)
 Definition foo : stateT unit option unit :=
diff --git a/theories/Core/Any.v b/theories/Core/Any.v
index 299120b4..9cc0fed4 100644
--- a/theories/Core/Any.v
+++ b/theories/Core/Any.v
@@ -10,4 +10,5 @@ Polymorphic Definition RESOLVE (T : Type) : Type := T.
 
 Existing Class RESOLVE.
 
+#[global]
 Hint Extern 0 (RESOLVE _) => unfold RESOLVE : typeclass_instances.
diff --git a/theories/Data/Eq.v b/theories/Data/Eq.v
index 2dae4fe3..998d40f3 100644
--- a/theories/Data/Eq.v
+++ b/theories/Data/Eq.v
@@ -4,6 +4,9 @@
 Set Implicit Arguments.
 Set Strict Implicit.
 
+(** For backwards compatibility with hint locality attributes. *)
+Set Warnings "-unsupported-attributes".
+
 Create HintDb eq_rw discriminated.
 
 Lemma eq_sym_eq
@@ -28,6 +31,7 @@ Lemma match_eq_sym_eq
 Proof.
   destruct pf. reflexivity.
 Defined.
+#[global]
 Hint Rewrite match_eq_sym_eq : eq_rw.
 
 Lemma match_eq_sym_eq'
@@ -40,6 +44,7 @@ Lemma match_eq_sym_eq'
 Proof.
   destruct pf. reflexivity.
 Defined.
+#[global]
 Hint Rewrite match_eq_sym_eq' : eq_rw.
 
 
@@ -73,6 +78,7 @@ Lemma eq_Const_eq
 Proof.
   destruct pf. reflexivity.
 Defined.
+#[global]
 Hint Rewrite eq_Const_eq : eq_rw.
 
 Lemma eq_Arr_eq
@@ -88,11 +94,13 @@ Lemma eq_Arr_eq
 Proof.
   destruct pf. reflexivity.
 Defined.
+#[global]
 Hint Rewrite eq_Arr_eq : eq_rw.
 
 Lemma eq_sym_eq_sym : forall (T : Type) (a b : T) (pf : a = b),
                         eq_sym (eq_sym pf) = pf.
 Proof. destruct pf. reflexivity. Defined.
+#[global]
 Hint Rewrite eq_sym_eq_sym : eq_rw.
 
 Ltac autorewrite_eq_rw :=
diff --git a/theories/Data/ListFirstnSkipn.v b/theories/Data/ListFirstnSkipn.v
index ad5e284c..33d95cc8 100644
--- a/theories/Data/ListFirstnSkipn.v
+++ b/theories/Data/ListFirstnSkipn.v
@@ -2,6 +2,9 @@ Require Import Coq.Lists.List.
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Lia.
 
+(** For backwards compatibility with hint locality attributes. *)
+Set Warnings "-unsupported-attributes".
+
 Lemma firstn_app_L : forall T n (a b : list T),
   n <= length a ->
   firstn n (a ++ b) = firstn n a.
@@ -45,6 +48,7 @@ Proof.
   simpl. replace (n - 0) with n; [ | lia ]. reflexivity.
 Qed.
 
+#[global]
 Hint Rewrite firstn_app_L firstn_app_R firstn_all firstn_0 firstn_cons using lia : list_rw.
 
 Lemma skipn_app_R : forall T n (a b : list T),
@@ -90,4 +94,5 @@ Proof.
   simpl. replace (n - 0) with n; [ | lia ]. reflexivity.
 Qed.
 
+#[global]
 Hint Rewrite skipn_app_L skipn_app_R skipn_0 skipn_all skipn_cons using lia : list_rw.
diff --git a/theories/Data/Option.v b/theories/Data/Option.v
index 153c9b17..d375a42d 100644
--- a/theories/Data/Option.v
+++ b/theories/Data/Option.v
@@ -14,6 +14,9 @@ Require Import ExtLib.Tactics.Consider.
 Set Implicit Arguments.
 Set Strict Implicit.
 
+(** For backwards compatibility with hint locality attributes. *)
+Set Warnings "-unsupported-attributes".
+
 Global Instance Foldable_option {T} : Foldable (option T) T :=
   fun _ f d v =>
     match v with
@@ -180,4 +183,5 @@ Proof.
   destruct pf. destruct val; reflexivity.
 Defined.
 
+#[global]
 Hint Rewrite eq_option_eq : eq_rw.
diff --git a/theories/Data/PList.v b/theories/Data/PList.v
index b80dedfe..d8b9ff1f 100644
--- a/theories/Data/PList.v
+++ b/theories/Data/PList.v
@@ -216,6 +216,7 @@ End pmap.
 
 Polymorphic Definition Functor_plist@{i} : Functor@{i i} plist@{i} :=
 {| fmap := @fmap_plist@{i i} |}.
+#[global]
 Existing Instance Functor_plist.
 
 
diff --git a/theories/Data/POption.v b/theories/Data/POption.v
index 928f6463..ce2de987 100644
--- a/theories/Data/POption.v
+++ b/theories/Data/POption.v
@@ -80,9 +80,11 @@ End poption_map.
 
 Definition Functor_poption@{i} : Functor@{i i} poption@{i} :=
 {| fmap := @fmap_poption@{i i} |}.
+#[global]
 Existing Instance Functor_poption.
 
 Definition Applicative_poption@{i} : Applicative@{i i} poption@{i} :=
 {| pure := @pSome@{i}
  ; ap   := @ap_poption |}.
+#[global]
 Existing Instance Applicative_poption.
diff --git a/theories/Data/SigT.v b/theories/Data/SigT.v
index f452367f..0e964658 100644
--- a/theories/Data/SigT.v
+++ b/theories/Data/SigT.v
@@ -7,6 +7,9 @@ Set Implicit Arguments.
 Set Strict Implicit.
 Set Printing Universes.
 
+(** For backwards compatibility with hint locality attributes. *)
+Set Warnings "-unsupported-attributes".
+
 Section injective.
   Variable T : Type.
   Variable F : T -> Type.
@@ -39,4 +42,5 @@ Lemma eq_sigT_rw
             end.
 Proof. destruct pf. destruct s; reflexivity. Qed.
 
+#[global]
 Hint Rewrite eq_sigT_rw : eq_rw.
diff --git a/theories/Generic/Ind.v b/theories/Generic/Ind.v
index 9c3763e4..2c2c6200 100644
--- a/theories/Generic/Ind.v
+++ b/theories/Generic/Ind.v
@@ -132,7 +132,9 @@ Ltac all_resolve :=
              | |- _ => solve [ eauto with typeclass_instances ]
            end.
 
+#[global]
 Hint Extern 0 (ProductResolve _ _) => all_resolve : typeclass_instances.
+#[global]
 Hint Extern 0 (VariantResolve _ _) => all_resolve : typeclass_instances.
 
 Definition comma_before (b : bool) (s : showM) : showM :=
diff --git a/theories/Programming/Eqv.v b/theories/Programming/Eqv.v
index 35547624..8bcd804a 100644
--- a/theories/Programming/Eqv.v
+++ b/theories/Programming/Eqv.v
@@ -9,6 +9,7 @@ Class EqvWF T :=
 { eqvWFEqv :> Eqv T
 ; eqvWFEquivalence :> Equivalence eqv
 }.
+#[global]
 Instance EqvWF_Build {T} {E:Eqv T} {EV:Equivalence eqv} : EqvWF T :=
   { eqvWFEqv := E ; eqvWFEquivalence := EV }.
 
diff --git a/theories/Programming/Injection.v b/theories/Programming/Injection.v
index 781e6953..14747c0d 100644
--- a/theories/Programming/Injection.v
+++ b/theories/Programming/Injection.v
@@ -9,10 +9,13 @@ Polymorphic Class Injection (x : Type) (t : Type) := inject : x -> t.
 Class Projection x t := { project : t -> x ; pmodify : (x -> x) -> (t -> t) }.
 *)
 
+#[global]
 Polymorphic Instance Injection_refl {T : Type} : Injection T T :=
 { inject := @id T }.
 
+#[global]
 Instance Injection_ascii_string : Injection ascii string :=
   { inject a := String a EmptyString }.
+#[global]
 Instance Injection_ascii_string_cons : Injection ascii (string -> string) :=
   { inject := String }.
diff --git a/theories/Programming/Le.v b/theories/Programming/Le.v
index 22231269..017fe04d 100644
--- a/theories/Programming/Le.v
+++ b/theories/Programming/Le.v
@@ -8,9 +8,11 @@ Definition neg_lte {T} {L:Lte T} (x:T) (y:T) : Prop := not (lte x y).
 Definition lt {T} {L:Lte T} x y := lte x y /\ ~lte y x.
 Definition neg_lt {T} {L:Lte T} x y := not (lt x y).
 
+#[global]
 Instance lt_RelDec {T} {L:Lte T} {RD:RelDec lte} : RelDec lt :=
   { rel_dec x y := (rel_dec x y && negb (rel_dec y x))%bool }.
 
+#[global]
 Instance lt_RelDecCorrect {T} {L:Lte T} {RD:RelDec lte} {RDC:RelDec_Correct RD}
   : RelDec_Correct lt_RelDec.
 Proof. constructor.
@@ -29,6 +31,7 @@ Class LteWF T :=
 ; lteWFPreOrder :> PreOrder lte
 }.
 
+#[global]
 Instance LteWF_Build {T} {L:Lte T} {PO:PreOrder lte} : LteWF T :=
   { lteWFLte := L ; lteWFPreOrder := PO }.
 
diff --git a/theories/Tactics/BoolTac.v b/theories/Tactics/BoolTac.v
index 06f46439..2e2a25d5 100644
--- a/theories/Tactics/BoolTac.v
+++ b/theories/Tactics/BoolTac.v
@@ -3,6 +3,10 @@ Require Import Coq.Bool.Bool.
 Set Implicit Arguments.
 Set Strict Implicit.
 
+(** For backwards compatibility with hint locality attributes. *)
+Set Warnings "-unsupported-attributes".
+
+#[global]
 Hint Rewrite negb_orb negb_andb negb_involutive if_negb : bool_rw.
 
 Lemma negb_true : forall a, negb a = true -> a = false.
@@ -56,4 +60,4 @@ Proof.
   intros.
   do_bool.
 Abort.
-*)
\ No newline at end of file
+*)
diff --git a/theories/Tactics/Consider.v b/theories/Tactics/Consider.v
index 72b40fd0..8023752a 100644
--- a/theories/Tactics/Consider.v
+++ b/theories/Tactics/Consider.v
@@ -101,6 +101,7 @@ Section from_rel_dec.
   Qed.
 End from_rel_dec.
 
+#[global]
 Hint Extern 10 (@Reflect (?f ?a ?b) _ _) =>
   eapply (@Reflect_RelDecCorrect _ _ (@Build_RelDec _ _ f) _) : typeclass_instances.
 

From aea8ad3902b289107b73ad6a642b61df372e67d0 Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Thu, 30 Jun 2022 20:42:29 -0400
Subject: [PATCH 24/43] Retire Coq 8.10

---
 .circleci/config.yml | 33 ++++++++++++---------------------
 meta.yml             | 15 ++++++---------
 2 files changed, 18 insertions(+), 30 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index f6b83502..a2f500f5 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -61,29 +61,20 @@ workflows:
   test:
     jobs:
     - build:
-        name: "Coq 8.8"
-        coq: "coqorg/coq:8.8"
+        name: "Coq 8.11"
+        coq: "coqorg/coq:8.11"
     - build:
-        name: "Coq 8.9"
-        coq: "coqorg/coq:8.9"
+        name: "Coq 8.12"
+        coq: "coqorg/coq:8.12"
     - build:
-        name: "Coq 8.10"
-        coq: "coqorg/coq:8.10"
+        name: "Coq 8.13"
+        coq: "coqorg/coq:8.13"
     - build:
-        name: "Coq 8.11-ocaml-4.11-flambda"
-        coq: "coqorg/coq:8.11-ocaml-4.11-flambda"
+        name: "Coq 8.14"
+        coq: "coqorg/coq:8.14"
     - build:
-        name: "Coq 8.12-ocaml-4.11-flambda"
-        coq: "coqorg/coq:8.12-ocaml-4.11-flambda"
+        name: "Coq 8.15"
+        coq: "coqorg/coq:8.15"
     - build:
-        name: "Coq 8.13-ocaml-4.12-flambda"
-        coq: "coqorg/coq:8.13-ocaml-4.12-flambda"
-    - build:
-        name: "Coq 8.14-ocaml-4.12-flambda"
-        coq: "coqorg/coq:8.14-ocaml-4.12-flambda"
-    - build:
-        name: "Coq 8.15-ocaml-4.12-flambda"
-        coq: "coqorg/coq:8.15-ocaml-4.12-flambda"
-    - build:
-        name: "Coq dev-ocaml-4.12-flambda"
-        coq: "coqorg/coq:dev-ocaml-4.12-flambda"
+        name: "Coq dev"
+        coq: "coqorg/coq:dev"
diff --git a/meta.yml b/meta.yml
index 13a49e04..81fc2bbc 100644
--- a/meta.yml
+++ b/meta.yml
@@ -32,15 +32,12 @@ supported_coq_versions:
   opam: '{ >= "8.8" }'
 
 tested_coq_opam_versions:
-  - version: '8.8'
-  - version: '8.9'
-  - version: '8.10'
-  - version: '8.11-ocaml-4.11-flambda'
-  - version: '8.12-ocaml-4.11-flambda'
-  - version: '8.13-ocaml-4.12-flambda'
-  - version: '8.14-ocaml-4.12-flambda'
-  - version: '8.15-ocaml-4.12-flambda'
-  - version: 'dev-ocaml-4.12-flambda'
+  - version: '8.11'
+  - version: '8.12'
+  - version: '8.13'
+  - version: '8.14'
+  - version: '8.15'
+  - version: 'dev'
 
 make_target: theories
 test_target: examples

From bf494bf3131ebc63b8d3ccbddeed9d8e0a269ffa Mon Sep 17 00:00:00 2001
From: Yishuai Li <yishuai@upenn.edu>
Date: Wed, 6 Jul 2022 17:29:08 -0400
Subject: [PATCH 25/43] Allow Coq 8.9

---
 .circleci/config.yml | 3 +++
 README.md            | 2 +-
 coq-ext-lib.opam     | 2 +-
 meta.yml             | 5 +++--
 4 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index a2f500f5..c4fbb0e4 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -60,6 +60,9 @@ 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"
diff --git a/README.md b/README.md
index fbc05265..c7540361 100644
--- a/README.md
+++ b/README.md
@@ -33,7 +33,7 @@ A collection of theories and plugins that may be useful in other Coq development
   - Gregory Malecha ([**@gmalecha**](https://github.com/gmalecha))
   - Yishuai Li ([**@liyishuai**](https://github.com/liyishuai))
 - License: [BSD 2-Clause "Simplified" License](LICENSE)
-- Compatible Coq versions: Coq 8.8 or later
+- Compatible Coq versions: Coq 8.11 or later or 8.9
 - Additional dependencies: none
 - Coq namespace: `ExtLib`
 - Related publication(s): none
diff --git a/coq-ext-lib.opam b/coq-ext-lib.opam
index 6f5abadd..8e703d20 100644
--- a/coq-ext-lib.opam
+++ b/coq-ext-lib.opam
@@ -16,7 +16,7 @@ install: [
 ]
 depends: [
   "ocaml"
-  "coq" {>= "8.8"}
+  "coq" { >= "8.9" < "8.10" | >= "8.11" }
 ]
 synopsis: "A library of Coq definitions, theorems, and tactics"
 description: """
diff --git a/meta.yml b/meta.yml
index 81fc2bbc..55a38cdb 100644
--- a/meta.yml
+++ b/meta.yml
@@ -28,10 +28,11 @@ license:
   identifier: BSD-2-Clause
 
 supported_coq_versions:
-  text: Coq 8.8 or later
-  opam: '{ >= "8.8" }'
+  text: Coq 8.11 or later or 8.9
+  opam: '{ >= "8.9" < "8.10" | >= "8.11" }'
 
 tested_coq_opam_versions:
+  - version: '8.9'
   - version: '8.11'
   - version: '8.12'
   - version: '8.13'

From a1b6f914b12d3f7c35741acc2f6c83f1a47813ba Mon Sep 17 00:00:00 2001
From: Andrej Dudenhefner <mrhaandi@gmail.com>
Date: Mon, 11 Jul 2022 14:57:11 +0200
Subject: [PATCH 26/43] improved auto goal selection (see coq/#16293)

---
 theories/Data/Map/FMapAList.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Data/Map/FMapAList.v b/theories/Data/Map/FMapAList.v
index 72b2f152..47c0bc41 100644
--- a/theories/Data/Map/FMapAList.v
+++ b/theories/Data/Map/FMapAList.v
@@ -53,7 +53,7 @@ Section keyed.
     induction m; intuition.
     unfold alist_find', compose.
     simpl.
-    destruct (k ?[ R ] a0) eqn:Heq; intuition.
+    destruct (k ?[ R ] a0) eqn:Heq; [intuition|].
     rewrite IHm.
     reflexivity.
   Qed.

From f2b709f46f5d7909648730393facb8f3cfc38a1d Mon Sep 17 00:00:00 2001
From: Li-yao Xia <lysxia@gmail.com>
Date: Fri, 19 Aug 2022 16:55:59 +0100
Subject: [PATCH 27/43] Re-add continuation monad

---
 theories/Data/Monads/ContMonad.v | 30 ++++++++++++++++--------------
 1 file changed, 16 insertions(+), 14 deletions(-)

diff --git a/theories/Data/Monads/ContMonad.v b/theories/Data/Monads/ContMonad.v
index e88b2502..509d1441 100644
--- a/theories/Data/Monads/ContMonad.v
+++ b/theories/Data/Monads/ContMonad.v
@@ -1,12 +1,12 @@
 Require Import ExtLib.Structures.Monad.
+Require Import ExtLib.Structures.MonadTrans.
 
 Set Implicit Arguments.
-Set Strict Implicit.
+Set Contextual Implicit.
+Set Maximal Implicit Insertion.
 
-(*
 Section ContType.
-  Variable Ans : Type.
-
+  Variable R : Type.
 
 (*
   Record cont (t : Type) : Type := mkCont
@@ -31,23 +31,19 @@ Section ContType.
     mkCont (fun x => runCont c (f x)).
 *)
 
-  Variable m : Type -> Type.
+  Variable M : Type -> Type.
 
-  Record contT (t : Type) : Type := mkContT
-  { runContT : (t -> m Ans) -> m Ans }.
+  Record contT (A : Type) : Type := mkContT
+  { runContT : (A -> M R) -> M R }.
 
   Global Instance Monad_contT : Monad contT :=
   { ret := fun _ x => mkContT (fun k => k x)
-  ; bind := fun _ c1 _ c2 =>
+  ; bind := fun _ _ c1 c2 =>
     mkContT (fun c =>
       runContT c1 (fun a => runContT (c2 a) c))
   }.
 
-  Global Instance Cont_contT : Cont contT :=
-  { callCC := fun _ _ f => mkContT (fun c => runContT (f (fun x => mkContT (fun _ => c x))) c)
-  }.
-
-  Global Instance MonadT_contT (M : Monad m) : MonadT contT m :=
+  Global Instance MonadT_contT {Monad_M : Monad M} : MonadT contT M :=
   { lift := fun _ c => mkContT (bind c)
   }.
 
@@ -60,4 +56,10 @@ Section ContType.
 *)
 
 End ContType.
-*)
\ No newline at end of file
+
+Definition resetT {M} {Monad_M : Monad M} {R R'} (u : contT R M R) : contT R' M R :=
+  mkContT (fun k => bind (runContT u ret) k).
+
+Definition shiftT {M} {Monad_M : Monad M} {R A}
+    (f : (A -> M R) -> contT R M R) : contT R M A :=
+  mkContT (fun k => runContT (f k) ret).

From d48e6583c4fe01479f743ea21d9b921073cb3f5b Mon Sep 17 00:00:00 2001
From: Yishuai Li <liyishuai.lys@alibaba-inc.com>
Date: Thu, 22 Sep 2022 16:04:16 +0800
Subject: [PATCH 28/43] v0.11.7 documentation

---
 meta.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/meta.yml b/meta.yml
index 55a38cdb..a07dccde 100644
--- a/meta.yml
+++ b/meta.yml
@@ -75,6 +75,7 @@ documentation: |
     - Base directory to the provided theories
 
 coqdoc_index: |
+  - [0.11.7](v0.11.7/toc.html)
   - [0.11.6](v0.11.6/toc.html)
   - [0.11.5](v0.11.5/toc.html)
   - [0.11.4](v0.11.4/toc.html)

From b3c05e7070882c774d5761efe4cf181873996fca Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres-github@andres.systems>
Date: Tue, 21 Feb 2023 16:53:16 +0000
Subject: [PATCH 29/43] adapt for coq/coq#17133

---
 theories/Data/HList.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Data/HList.v b/theories/Data/HList.v
index f6e49971..0c15cb79 100644
--- a/theories/Data/HList.v
+++ b/theories/Data/HList.v
@@ -678,7 +678,7 @@ Section hlist.
           (projT2 x) (hlist_app vs vs') = y vs'.
   Proof.
     clear. induction tvs; simpl; intros.
-    { rewrite <- Minus.minus_n_O.
+    { rewrite PeanoNat.Nat.sub_0_r.
       rewrite H0. destruct x. simpl.
       eexists; split; eauto. intros.
       rewrite (hlist_eta vs). reflexivity. }

From 258c7c875ffc1fc7c9a6463576d06b2183856576 Mon Sep 17 00:00:00 2001
From: Yishuai Li <liyishuai.lys@alibaba-inc.com>
Date: Thu, 9 Mar 2023 11:16:48 +0800
Subject: [PATCH 30/43] CI: diverge from template to skip dependants

---
 .circleci/config.yml | 7 ++++---
 meta.yml             | 2 +-
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index c4fbb0e4..e1065246 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -1,6 +1,3 @@
-# This file was generated from `meta.yml`, please do not edit manually.
-# Follow the instructions on https://github.com/coq-community/templates to regenerate.
-
 version: 2.1
 
 jobs:
@@ -16,6 +13,8 @@ jobs:
       OPAMVERBOSE: 1
       OPAMYES: true
       TERM: xterm
+      SKIP_BUILD: |
+        coq-certicoq
     steps:
     - checkout
     - run:
@@ -49,6 +48,8 @@ jobs:
           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
diff --git a/meta.yml b/meta.yml
index a07dccde..32f29d9e 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: true
+circleci: false
 ci_test_dependants: true
 submodule: true
 

From 5f48fb36d6bf351ba3ed99d2dc7a1a1efef3a502 Mon Sep 17 00:00:00 2001
From: Yishuai Li <liyishuai.lys@alibaba-inc.com>
Date: Thu, 9 Mar 2023 12:03:51 +0800
Subject: [PATCH 31/43] CI: Coq 8.16 and 8.17

---
 .circleci/config.yml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index e1065246..12fd3006 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -79,6 +79,12 @@ workflows:
     - 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"

From 4811a83db9ccd81f4dcbf77eeff0484dfb21a48b Mon Sep 17 00:00:00 2001
From: Yishuai Li <liyishuai.lys@alibaba-inc.com>
Date: Thu, 9 Mar 2023 13:14:11 +0800
Subject: [PATCH 32/43] v0.11.8 documentation

---
 meta.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/meta.yml b/meta.yml
index 32f29d9e..6a334c75 100644
--- a/meta.yml
+++ b/meta.yml
@@ -75,6 +75,7 @@ documentation: |
     - Base directory to the provided theories
 
 coqdoc_index: |
+  - [0.11.8](v0.11.8/toc.html)
   - [0.11.7](v0.11.7/toc.html)
   - [0.11.6](v0.11.6/toc.html)
   - [0.11.5](v0.11.5/toc.html)

From 5a5cfa723e293f173fa25c07da6424b3a9791020 Mon Sep 17 00:00:00 2001
From: Yishuai Li <liyishuai.lys@alibaba-inc.com>
Date: Fri, 10 Mar 2023 14:40:25 +0800
Subject: [PATCH 33/43] CI: GitHub Actions

---
 .circleci/config.yml                | 90 -----------------------------
 .github/workflows/docker-action.yml | 70 ++++++++++++++++++++++
 README.md                           |  6 +-
 meta.yml                            |  9 ++-
 4 files changed, 81 insertions(+), 94 deletions(-)
 delete mode 100644 .circleci/config.yml
 create mode 100644 .github/workflows/docker-action.yml

diff --git a/.circleci/config.yml b/.circleci/config.yml
deleted file mode 100644
index 12fd3006..00000000
--- 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 00000000..f6d0ece2
--- /dev/null
+++ b/.github/workflows/docker-action.yml
@@ -0,0 +1,70 @@
+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:
+          - 'coqorg/coq:8.9'
+          - 'coqorg/coq:8.11'
+          - 'coqorg/coq:8.12'
+          - 'coqorg/coq:8.13'
+          - 'coqorg/coq:8.14'
+          - 'coqorg/coq:8.15'
+          - 'coqorg/coq:8.16'
+          - 'coqorg/coq:8.17'
+          - 'coqorg/coq: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'
+          custom_image: ${{ matrix.image }}
+          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"
+              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 -y --deps-only $PACKAGE || DEPS_FAILED=true
+                 [ $DEPS_FAILED == true ] || opam install -t $PACKAGE
+              done
+            endGroup
+          export: 'OPAMWITHTEST'
+        env:
+          OPAMWITHTEST: true
+      - 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/README.md b/README.md
index c7540361..05e650e4 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/meta.yml b/meta.yml
index 6a334c75..6b057822 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
   -----

From 8a7a3d6aaa029a10ec4555378ac3992da99770e7 Mon Sep 17 00:00:00 2001
From: Yishuai Li <liyishuai.lys@alibaba-inc.com>
Date: Fri, 10 Mar 2023 15:35:34 +0800
Subject: [PATCH 34/43] Deprecate duplicated definitions

---
 .github/workflows/docker-action.yml |  6 ++--
 theories/Data/Char.v                | 18 ++++++----
 theories/Data/String.v              | 55 ++++++++++++++++-------------
 theories/Programming/Extras.v       | 38 +++++++++++++-------
 4 files changed, 72 insertions(+), 45 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index f6d0ece2..54a979d5 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -45,17 +45,19 @@ jobs:
             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 -y --deps-only $PACKAGE || DEPS_FAILED=true
+                 opam install --deps-only $PACKAGE || DEPS_FAILED=true
                  [ $DEPS_FAILED == true ] || opam install -t $PACKAGE
               done
             endGroup
-          export: 'OPAMWITHTEST'
+          export: 'OPAMWITHTEST OPAMCONFIRMLEVEL'
         env:
           OPAMWITHTEST: true
+          OPAMCONFIRMLEVEL: unsafe-yes
       - name: Revert permissions
         # to avoid a warning at cleanup time
         if: ${{ always() }}
diff --git a/theories/Data/Char.v b/theories/Data/Char.v
index 29308938..53199ba3 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 052df919..368df8a6 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 7bf9c2ce..bdfd18f1 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.

From 995151f6df3768625922c3b2be5d9f4801b3dd3f Mon Sep 17 00:00:00 2001
From: Yishuai Li <liyishuai.lys@alibaba-inc.com>
Date: Tue, 13 Jun 2023 10:27:14 +0800
Subject: [PATCH 35/43] CoqdocJs master branch

---
 .github/workflows/docker-action.yml | 22 +++++++++++-----------
 Makefile                            |  1 +
 coqdocjs                            |  2 +-
 3 files changed, 13 insertions(+), 12 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 54a979d5..3e804ac5 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -14,16 +14,16 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        image:
-          - 'coqorg/coq:8.9'
-          - 'coqorg/coq:8.11'
-          - 'coqorg/coq:8.12'
-          - 'coqorg/coq:8.13'
-          - 'coqorg/coq:8.14'
-          - 'coqorg/coq:8.15'
-          - 'coqorg/coq:8.16'
-          - 'coqorg/coq:8.17'
-          - 'coqorg/coq:dev'
+        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
@@ -32,7 +32,7 @@ jobs:
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-ext-lib.opam'
-          custom_image: ${{ matrix.image }}
+          coq_version: ${{ matrix.coq }}
           before_script: |
             startGroup "Workaround permission issue"
               sudo chown -R coq:coq .
diff --git a/Makefile b/Makefile
index 2a04800c..70345710 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/coqdocjs b/coqdocjs
index 556b3ab2..57401849 160000
--- a/coqdocjs
+++ b/coqdocjs
@@ -1 +1 @@
-Subproject commit 556b3ab2a3199237cde937fe8ac196cf76099eb8
+Subproject commit 57401849fffb24500c078973a8382dd3086fd2bf

From faaab572145d63bb185e7aad6d86b91205897363 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 4 Jul 2023 17:29:55 +0200
Subject: [PATCH 36/43] Adapt to coq/coq#17795 (Polymorphic Class does not auto
 lower to Prop)

---
 theories/Core/Any.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Core/Any.v b/theories/Core/Any.v
index 9cc0fed4..ee71ea1d 100644
--- a/theories/Core/Any.v
+++ b/theories/Core/Any.v
@@ -2,7 +2,7 @@ Set Implicit Arguments.
 Set Strict Implicit.
 
 (** This class should be used when no requirements are needed **)
-Polymorphic Class Any (T : Type) : Type.
+Polymorphic Class Any (T : Type) : Prop.
 
 Global Polymorphic Instance Any_a (T : Type) : Any T := {}.
 

From edd30277e476892b50ea73f229536179a264886d Mon Sep 17 00:00:00 2001
From: Yishuai Li <liyishuai.lys@alibaba-inc.com>
Date: Tue, 19 Sep 2023 16:03:58 +0800
Subject: [PATCH 37/43] Create stale.yml

---
 .github/workflows/stale.yml | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 .github/workflows/stale.yml

diff --git a/.github/workflows/stale.yml b/.github/workflows/stale.yml
new file mode 100644
index 00000000..a88b3093
--- /dev/null
+++ b/.github/workflows/stale.yml
@@ -0,0 +1,14 @@
+name: 'Close stale issues and PRs'
+on:
+  schedule:
+    - cron: '30 1 * * 1-5'
+
+permissions:
+  issues: write
+  pull-requests: write
+
+jobs:
+  stale:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/stale@v8

From 3d4f7dfb733e7aa7defbde90a2702e98a954cc3a Mon Sep 17 00:00:00 2001
From: Yishuai Li <liyishuai.lys@alibaba-inc.com>
Date: Wed, 20 Sep 2023 14:59:35 +0800
Subject: [PATCH 38/43] Update stale.yml

---
 .github/workflows/stale.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/stale.yml b/.github/workflows/stale.yml
index a88b3093..bdd1fc51 100644
--- a/.github/workflows/stale.yml
+++ b/.github/workflows/stale.yml
@@ -12,3 +12,5 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/stale@v8
+        with:
+          days-before-close: -1

From 26626fa42c0c8a488522781bf867607531c4528e Mon Sep 17 00:00:00 2001
From: Pierre Rousselin <rousselin@math.univ-paris13.fr>
Date: Sat, 21 Oct 2023 18:47:49 +0200
Subject: [PATCH 39/43] Adapt to Coq/Coq#18164

We remove some Arith files and NPeano from the stdlib after deprecation.
---
 examples/ConsiderDemo.v     | 19 +++++++++----------
 theories/Data/HList.v       |  4 ++--
 theories/Data/ListNth.v     | 20 ++++++++++----------
 theories/Data/Nat.v         | 22 ++++++++++------------
 theories/Data/String.v      | 15 +++++++--------
 theories/Programming/Show.v |  8 ++++----
 6 files changed, 42 insertions(+), 46 deletions(-)

diff --git a/examples/ConsiderDemo.v b/examples/ConsiderDemo.v
index 20c1f404..542a935d 100644
--- a/examples/ConsiderDemo.v
+++ b/examples/ConsiderDemo.v
@@ -1,6 +1,5 @@
 Require Import Coq.Bool.Bool.
-Require NPeano.
-Import NPeano.Nat.
+Require Import Arith.PeanoNat.
 Require Import ExtLib.Tactics.Consider.
 Require Import ExtLib.Data.Nat.
 
@@ -12,19 +11,19 @@ Set Strict Implicit.
 
 (**  Some tests *)
 Section test.
-  Goal forall x y z,  (ltb x y && ltb y z) = true ->
-                 ltb x z = true.
+  Goal forall x y z,  (Nat.ltb x y && Nat.ltb y z) = true ->
+                 Nat.ltb x z = true.
   intros x y z.
-  consider (ltb x y && ltb y z).
-  consider (ltb x z); auto. intros. exfalso. lia.
+  consider (Nat.ltb x y && Nat.ltb y z).
+  consider (Nat.ltb x z); auto. intros. exfalso. lia.
   Qed.
 
   Goal forall x y z,
-    ltb x y = true ->
-    ltb y z = true ->
-    ltb x z = true.
+    Nat.ltb x y = true ->
+    Nat.ltb y z = true ->
+    Nat.ltb x z = true.
   Proof.
-    intros. consider (ltb x y); consider (ltb y z); consider (ltb x z); intros; auto.
+    intros. consider (Nat.ltb x y); consider (Nat.ltb y z); consider (Nat.ltb x z); intros; auto.
     exfalso; lia.
   Qed.
 
diff --git a/theories/Data/HList.v b/theories/Data/HList.v
index 0c15cb79..6ec17186 100644
--- a/theories/Data/HList.v
+++ b/theories/Data/HList.v
@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List.
+Require Import Coq.Lists.List Coq.Arith.PeanoNat.
 Require Import Relations RelationClasses.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Data.SigT.
@@ -658,7 +658,7 @@ Section hlist.
       { clear H IHtvs.
         eexists; split; eauto. eexists; split; eauto.
         simpl. intros. rewrite (hlist_eta vs). reflexivity. }
-      { apply Lt.lt_S_n in H.
+      { apply Nat.succ_lt_mono in H.
         { specialize (IHtvs _ H).
           forward_reason.
           rewrite H0. rewrite H1.
diff --git a/theories/Data/ListNth.v b/theories/Data/ListNth.v
index de2502e4..a4a7c0f4 100644
--- a/theories/Data/ListNth.v
+++ b/theories/Data/ListNth.v
@@ -1,5 +1,5 @@
 Require Import Coq.Lists.List.
-Require Import Coq.Arith.Lt Coq.Arith.Plus.
+Require Import Coq.Arith.PeanoNat.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -14,7 +14,7 @@ Section parametric.
     induction A; destruct n; simpl; intros; auto.
     { inversion H. }
     { inversion H. }
-    { eapply IHA. apply Lt.lt_S_n; assumption. }
+    { eapply IHA. apply Nat.succ_lt_mono; assumption. }
   Qed.
 
   Lemma nth_error_app_R : forall (A B : list T) n,
@@ -23,7 +23,7 @@ Section parametric.
   Proof.
     induction A; destruct n; simpl; intros; auto.
     + inversion H.
-    + apply IHA. apply Le.le_S_n; assumption.
+    + apply IHA. apply Nat.succ_le_mono; assumption.
   Qed.
 
   Lemma nth_error_weaken : forall ls' (ls : list T) n v,
@@ -45,15 +45,15 @@ Section parametric.
   Proof.
     clear. induction ls; destruct n; simpl; intros; auto.
     + inversion H.
-    + apply IHls. apply Le.le_S_n; assumption.
+    + apply IHls. apply Nat.succ_le_mono; assumption.
   Qed.
 
   Lemma nth_error_length : forall (ls ls' : list T) n,
     nth_error (ls ++ ls') (n + length ls) = nth_error ls' n.
   Proof.
     induction ls; simpl; intros.
-    rewrite Plus.plus_0_r. auto.
-    rewrite <- Plus.plus_Snm_nSm.
+    rewrite Nat.add_0_r. auto.
+    rewrite <-Nat.add_succ_comm.
     simpl. eapply IHls.
   Qed.
 
@@ -61,9 +61,9 @@ Section parametric.
     nth_error ls n = None -> length ls <= n.
   Proof.
     induction ls; destruct n; simpl in *; auto; simpl in *.
-    + intro. apply Le.le_0_n.
+    + intro. apply Nat.le_0_l.
     + inversion 1.
-    + intros. eapply Le.le_n_S. auto.
+    + intros. apply ->Nat.succ_le_mono. auto.
   Qed.
 
   Lemma nth_error_length_lt : forall {T} (ls : list T) n val,
@@ -72,8 +72,8 @@ Section parametric.
     induction ls; destruct n; simpl; intros; auto.
     + inversion H.
     + inversion H.
-    + apply Lt.lt_0_Sn.
-    + apply Lt.lt_n_S. eauto.
+    + apply Nat.lt_0_succ.
+    + apply ->Nat.succ_lt_mono. apply IHls with (1 := H).
   Qed.
 
 
diff --git a/theories/Data/Nat.v b/theories/Data/Nat.v
index 49e0beba..7c81bac2 100644
--- a/theories/Data/Nat.v
+++ b/theories/Data/Nat.v
@@ -9,47 +9,45 @@ Set Strict Implicit.
 
 
 Global Instance RelDec_eq : RelDec (@eq nat) :=
-{ rel_dec := EqNat.beq_nat }.
-
-Require Coq.Numbers.Natural.Peano.NPeano.
+{ rel_dec := Nat.eqb }.
 
 Global Instance RelDec_lt : RelDec lt :=
-{ rel_dec := NPeano.Nat.ltb }.
+{ rel_dec := Nat.ltb }.
 
 Global Instance RelDec_le : RelDec le :=
-{ rel_dec := NPeano.Nat.leb }.
+{ rel_dec := Nat.leb }.
 
 Global Instance RelDec_gt : RelDec gt :=
-{ rel_dec := fun x y => NPeano.Nat.ltb y x }.
+{ rel_dec := fun x y => Nat.ltb y x }.
 
 Global Instance RelDec_ge : RelDec ge :=
-{ rel_dec := fun x y => NPeano.Nat.leb y x }.
+{ rel_dec := fun x y => Nat.leb y x }.
 
 Global Instance RelDecCorrect_eq : RelDec_Correct RelDec_eq.
 Proof.
-  constructor; simpl. apply EqNat.beq_nat_true_iff.
+  constructor; simpl. apply PeanoNat.Nat.eqb_eq.
 Qed.
 
 Global Instance RelDecCorrect_lt : RelDec_Correct RelDec_lt.
 Proof.
-  constructor; simpl. eapply NPeano.Nat.ltb_lt.
+  constructor; simpl. eapply PeanoNat.Nat.ltb_lt.
 Qed.
 
 Global Instance RelDecCorrect_le : RelDec_Correct RelDec_le.
 Proof.
-  constructor; simpl. eapply NPeano.Nat.leb_le.
+  constructor; simpl. eapply PeanoNat.Nat.leb_le.
 Qed.
 
 Global Instance RelDecCorrect_gt : RelDec_Correct RelDec_gt.
 Proof.
   constructor; simpl. unfold rel_dec; simpl.
-  intros. eapply NPeano.Nat.ltb_lt.
+  intros. eapply PeanoNat.Nat.ltb_lt.
 Qed.
 
 Global Instance RelDecCorrect_ge : RelDec_Correct RelDec_ge.
 Proof.
   constructor; simpl. unfold rel_dec; simpl.
-  intros. eapply NPeano.Nat.leb_le.
+  intros. eapply PeanoNat.Nat.leb_le.
 Qed.
 
 Inductive R_nat_S : nat -> nat -> Prop :=
diff --git a/theories/Data/String.v b/theories/Data/String.v
index 368df8a6..98f8269f 100644
--- a/theories/Data/String.v
+++ b/theories/Data/String.v
@@ -1,7 +1,6 @@
 Require Import Coq.Strings.String.
 Require Import Coq.Program.Program. 
-Require Import Coq.Numbers.Natural.Peano.NPeano.
-Require Import Coq.Arith.Arith.
+Require Import Coq.Arith.PeanoNat.
 
 Require Import ExtLib.Tactics.Consider.
 Require Import ExtLib.Core.RelDec.
@@ -99,19 +98,19 @@ Section Program_Scope.
     destruct n; destruct m; intros.
     inversion H. exfalso. apply H0. etransitivity. 2: eassumption. repeat constructor.
     inversion H.
-    eapply neq_0_lt. congruence.
+    now apply Nat.lt_0_succ.
   Qed.
 
   Program Fixpoint nat2string (n:nat) {measure n}: string :=
-    match NPeano.Nat.ltb n modulus as x return NPeano.Nat.ltb n modulus = x -> string with
+    match Nat.ltb n modulus as x return Nat.ltb n modulus = x -> string with
       | true => fun _ => String (digit2ascii n) EmptyString
       | false => fun pf =>
-        let m := NPeano.Nat.div n modulus in
+        let m := Nat.div n modulus in
         append (nat2string m) (String (digit2ascii (n - modulus * m)) EmptyString)
-    end (@Logic.eq_refl _ (NPeano.Nat.ltb n modulus)).
+    end (@Logic.eq_refl _ (Nat.ltb n modulus)).
   Next Obligation.
-    eapply NPeano.Nat.div_lt; auto.
-    consider (NPeano.Nat.ltb n modulus); try congruence. intros.
+    eapply Nat.div_lt; auto.
+    consider (Nat.ltb n modulus); try congruence. intros.
     eapply _xxx; eassumption.
   Defined.
 
diff --git a/theories/Programming/Show.v b/theories/Programming/Show.v
index 4203fe7d..f0f056f7 100644
--- a/theories/Programming/Show.v
+++ b/theories/Programming/Show.v
@@ -172,12 +172,12 @@ Section hiding_notation.
     if Compare_dec.le_gt_dec n 9 then
       inject (Char.digit2ascii n)
     else
-      let n' := NPeano.Nat.div n 10 in
+      let n' := Nat.div n 10 in
       (@nat_show n' _) << (inject (Char.digit2ascii (n - 10 * n'))).
   Next Obligation.
-    assert (NPeano.Nat.div n 10 < n) ; eauto.
-    eapply NPeano.Nat.div_lt.
-    match goal with [ H : n > _ |- _ ] => inversion H end; apply Lt.lt_O_Sn.
+    assert (Nat.div n 10 < n) ; eauto.
+    eapply Nat.div_lt.
+    match goal with [ H : n > _ |- _ ] => inversion H end; apply Nat.lt_0_succ.
     repeat constructor.
   Defined.
   Global Instance nat_Show : Show nat := { show := nat_show }.

From 2c72dfd7db4deb90453ccea068299f49243f777a Mon Sep 17 00:00:00 2001
From: Yishuai Li <liyishuai.lys@alibaba-inc.com>
Date: Tue, 24 Oct 2023 11:35:36 +0800
Subject: [PATCH 40/43] Fix Makefile for CoqdocJS

---
 .github/workflows/docker-action.yml | 2 +-
 coq-ext-lib.opam                    | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 3e804ac5..8c4d0ae9 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -41,7 +41,7 @@ jobs:
             set -o pipefail  # recommended if the script uses pipes
 
             startGroup "Generate Coqdoc"
-              make -j`nproc` html
+              make -j`nproc` coqdoc
             endGroup
 
             startGroup "Test dependants"
diff --git a/coq-ext-lib.opam b/coq-ext-lib.opam
index 8e703d20..bc5a33c2 100644
--- a/coq-ext-lib.opam
+++ b/coq-ext-lib.opam
@@ -1,5 +1,6 @@
 opam-version: "2.0"
 maintainer: "gmalecha@gmail.com"
+version: "dev"
 homepage: "https://github.com/coq-community/coq-ext-lib"
 dev-repo: "git+https://github.com/coq-community/coq-ext-lib.git"
 bug-reports: "https://github.com/coq-community/coq-ext-lib/issues"

From d66cc013d3e714e5eba1e9ea3f4713f0218d9232 Mon Sep 17 00:00:00 2001
From: Yishuai Li <liyishuai.lys@alibaba-inc.com>
Date: Tue, 24 Oct 2023 12:20:46 +0800
Subject: [PATCH 41/43] OPAM and workflow from template

---
 .github/workflows/docker-action.yml | 46 ++++++++++++++---------------
 coq-ext-lib.opam                    | 33 ++++++++++-----------
 meta.yml                            | 32 ++++++++++++--------
 3 files changed, 59 insertions(+), 52 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 8c4d0ae9..67c62f04 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -1,3 +1,5 @@
+# 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:
@@ -14,16 +16,16 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        coq:
-          - '8.9'
-          - '8.11'
-          - '8.12'
-          - '8.13'
-          - '8.14'
-          - '8.15'
-          - '8.16'
-          - '8.17'
-          - 'dev'
+        image:
+          - 'coqorg/coq:8.9'
+          - 'coqorg/coq:8.11'
+          - 'coqorg/coq:8.12'
+          - 'coqorg/coq:8.13'
+          - 'coqorg/coq:8.14'
+          - 'coqorg/coq:8.15'
+          - 'coqorg/coq:8.16'
+          - 'coqorg/coq:8.17'
+          - 'coqorg/coq:dev'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3
@@ -32,28 +34,26 @@ jobs:
       - 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
+          custom_image: ${{ matrix.image }}
           after_script: |
-            set -o pipefail  # recommended if the script uses pipes
-
-            startGroup "Generate Coqdoc"
-              make -j`nproc` coqdoc
-            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
+                 opam install -y --deps-only $PACKAGE || DEPS_FAILED=true
                  [ $DEPS_FAILED == true ] || opam install -t $PACKAGE
               done
             endGroup
+            set -o pipefail  # recommended if the script uses pipes
+
+            startGroup "Generate Coqdoc"
+              make -j`nproc` coqdoc
+            endGroup
+          before_script: |
+            startGroup "Workaround permission issue"
+              sudo chown -R coq:coq .
+            endGroup
           export: 'OPAMWITHTEST OPAMCONFIRMLEVEL'
         env:
           OPAMWITHTEST: true
diff --git a/coq-ext-lib.opam b/coq-ext-lib.opam
index bc5a33c2..39257a06 100644
--- a/coq-ext-lib.opam
+++ b/coq-ext-lib.opam
@@ -1,30 +1,29 @@
+# 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: "gmalecha@gmail.com"
 version: "dev"
+
 homepage: "https://github.com/coq-community/coq-ext-lib"
 dev-repo: "git+https://github.com/coq-community/coq-ext-lib.git"
 bug-reports: "https://github.com/coq-community/coq-ext-lib/issues"
-authors: ["Gregory Malecha"]
 license: "BSD-2-Clause"
-build: [
-  [make "-j%{jobs}%" "theories"]
-]
-run-test: [
-  [make "-j%{jobs}%" "examples"]
-]
-install: [
-  [make "install"]
-]
-depends: [
-  "ocaml"
-  "coq" { >= "8.9" < "8.10" | >= "8.11" }
-]
+
 synopsis: "A library of Coq definitions, theorems, and tactics"
 description: """
 A collection of theories and plugins that may be useful in other Coq developments."""
+
+build: [make "-j%{jobs}%" "theories"]
+run-test: [make "-j%{jobs}%" "examples"]
+install: [make "install"]
+depends: [
+  "coq" { >= "8.9" < "8.10" | >= "8.11" }
+]
+
 tags: [
   "logpath:ExtLib"
 ]
-url {
-  src: "git+https://github.com/coq-community/coq-ext-lib"
-}
+authors: [
+  "Gregory Malecha"
+]
diff --git a/meta.yml b/meta.yml
index 6b057822..3ac6437a 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
-action: false
+action: true
 ci_test_dependants: true
 submodule: true
 
@@ -46,20 +46,28 @@ make_target: theories
 test_target: examples
 namespace: ExtLib
 
-circleci_after_script: |2-
-      - run:
-          name: Generate Coqdoc
-          command: |
-            make -j`nproc` html
-            tar cfz coqdoc.tgz html
-      - store_artifacts:
-          path: coqdoc.tgz
-
 action_appendix: |2-
-            export: 'OPAMWITHTEST'
+              set -o pipefail  # recommended if the script uses pipes
+
+              startGroup "Generate Coqdoc"
+                make -j`nproc` coqdoc
+              endGroup
+            before_script: |
+              startGroup "Workaround permission issue"
+                sudo chown -R coq:coq .
+              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
 documentation: |
   Ideas
   -----

From eed3062bb725347881e68d93134ad97c37a6fe64 Mon Sep 17 00:00:00 2001
From: Yishuai Li <liyishuai.lys@alibaba-inc.com>
Date: Tue, 24 Oct 2023 15:07:47 +0800
Subject: [PATCH 42/43] CI: install Clang

---
 .github/workflows/docker-action.yml | 3 +++
 meta.yml                            | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 67c62f04..26995515 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -51,6 +51,9 @@ jobs:
               make -j`nproc` coqdoc
             endGroup
           before_script: |
+            startGroup "Install and configure Clang"
+              opam install conf-clang
+            endGroup
             startGroup "Workaround permission issue"
               sudo chown -R coq:coq .
             endGroup
diff --git a/meta.yml b/meta.yml
index 3ac6437a..bc1babeb 100644
--- a/meta.yml
+++ b/meta.yml
@@ -53,6 +53,9 @@ action_appendix: |2-
                 make -j`nproc` coqdoc
               endGroup
             before_script: |
+              startGroup "Install and configure Clang"
+                opam install conf-clang
+              endGroup
               startGroup "Workaround permission issue"
                 sudo chown -R coq:coq .
               endGroup

From 00d3f4e2a260c7c23d2c0b9cbc69516f8be4ac92 Mon Sep 17 00:00:00 2001
From: Yishuai Li <liyishuai.lys@alibaba-inc.com>
Date: Tue, 24 Oct 2023 12:42:20 +0800
Subject: [PATCH 43/43] Remove deprecated definitions

---
 .github/workflows/docker-action.yml |  1 +
 meta.yml                            |  1 +
 theories/Data/Char.v                | 39 -----------------------------
 theories/Data/String.v              | 24 ------------------
 4 files changed, 2 insertions(+), 63 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 26995515..be5a68c2 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -25,6 +25,7 @@ jobs:
           - 'coqorg/coq:8.15'
           - 'coqorg/coq:8.16'
           - 'coqorg/coq:8.17'
+          - 'coqorg/coq:8.18'
           - 'coqorg/coq:dev'
       fail-fast: false
     steps:
diff --git a/meta.yml b/meta.yml
index bc1babeb..038a8ff2 100644
--- a/meta.yml
+++ b/meta.yml
@@ -40,6 +40,7 @@ tested_coq_opam_versions:
   - version: '8.15'
   - version: '8.16'
   - version: '8.17'
+  - version: '8.18'
   - version: 'dev'
 
 make_target: theories
diff --git a/theories/Data/Char.v b/theories/Data/Char.v
index 53199ba3..b144b0de 100644
--- a/theories/Data/Char.v
+++ b/theories/Data/Char.v
@@ -6,45 +6,6 @@ Require Import ExtLib.Core.RelDec.
 Set Implicit Arguments.
 Set Strict Implicit.
 
-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 =>
-      if Bool.eqb l1 r1 then
-      if Bool.eqb l2 r2 then
-      if Bool.eqb l3 r3 then
-      if Bool.eqb l4 r4 then
-      if Bool.eqb l5 r5 then
-      if Bool.eqb l6 r6 then
-      if Bool.eqb l7 r7 then
-      if Bool.eqb l8 r8 then true
-        else false
-        else false
-        else false
-        else false
-        else false
-        else false
-        else false
-        else false
-  end.
-
-#[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.
-  destruct l; destruct r.
-  repeat match goal with
-           | [ |- (if ?X then _ else _) = true <-> _ ] =>
-             consider X; intros; subst
-         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.eqb }.
 
diff --git a/theories/Data/String.v b/theories/Data/String.v
index 98f8269f..954a956c 100644
--- a/theories/Data/String.v
+++ b/theories/Data/String.v
@@ -39,30 +39,6 @@ Definition deprecated_ascii_cmp (l r : Ascii.ascii) : comparison :=
 #[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.eqb l r then deprecated_string_dec ls rs
-      else false
-    | _ , _ => false
-  end.
-
-#[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; 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.eqb |}.