diff --git a/.circleci/config.yml b/.circleci/config.yml
deleted file mode 100644
index 8005e94f..00000000
--- a/.circleci/config.yml
+++ /dev/null
@@ -1,79 +0,0 @@
-version: 2.1
-
-jobs:
-  build:
-    parameters:
-      coq:
-        type: string
-    docker:
-    - image: <<parameters.coq>>
-    resource_class: medium
-    environment:
-      OPAMJOBS: 2
-      OPAMVERBOSE: 1
-      OPAMYES: true
-      TERM: xterm
-    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 repo -a --set-default add coq-extra-dev https://coq.inria.fr/opam/extra-dev
-          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`
-          if [ -n "$PACKAGES" ]
-          then opam install -t $PACKAGES
-          fi
-    - run:
-        name: Uninstall package
-        command: opam uninstall .
-
-workflows:
-  version: 2
-  test:
-    jobs:
-    - build:
-        name: "Coq 8.8"
-        coq: "coqorg/coq:8.8"
-    - build:
-        name: "Coq 8.9"
-        coq: "coqorg/coq:8.9"
-    - build:
-        name: "Coq 8.10"
-        coq: "coqorg/coq:8.10"
-    - 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 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..be5a68c2
--- /dev/null
+++ b/.github/workflows/docker-action.yml
@@ -0,0 +1,76 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+name: Docker CI
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build:
+    # the OS must be GNU/Linux to be able to use the docker-coq-action
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - '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:8.18'
+          - '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 }}
+          after_script: |
+            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
+            set -o pipefail  # recommended if the script uses pipes
+
+            startGroup "Generate Coqdoc"
+              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
+          export: 'OPAMWITHTEST OPAMCONFIRMLEVEL'
+        env:
+          OPAMWITHTEST: true
+          OPAMCONFIRMLEVEL: unsafe-yes
+      - name: Revert permissions
+        # to avoid a warning at cleanup time
+        if: ${{ always() }}
+        run: sudo chown -R 1001:116 .
+      - uses: actions/upload-artifact@v3
+        with:
+          name: coqdoc
+          path: html
+
+# See also:
+# https://github.com/coq-community/docker-coq-action#readme
+# https://github.com/erikmd/docker-coq-github-action-demo
diff --git a/.github/workflows/stale.yml b/.github/workflows/stale.yml
new file mode 100644
index 00000000..bdd1fc51
--- /dev/null
+++ b/.github/workflows/stale.yml
@@ -0,0 +1,16 @@
+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
+        with:
+          days-before-close: -1
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/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/Makefile b/Makefile
index 2e7ece93..70345710 100644
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,6 @@
 all: theories examples
 
+COQDOCJS_LN?=true
 -include coqdocjs/Makefile.doc
 COQMAKEFILE?=Makefile.coq
 
@@ -28,10 +29,14 @@ dist:
 
 .PHONY: all clean dist theories examples html
 
-TEMPLATES ?= ../templates
+TEMPLATES ?= templates
 
 index.html: index.md
 	pandoc -s $^ -o $@
 
 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
diff --git a/README.md b/README.md
index 1fe3370c..05e650e4 100644
--- a/README.md
+++ b/README.md
@@ -1,12 +1,16 @@
+<!---
+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]
+[![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
@@ -28,8 +32,8 @@ 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)
-- Compatible Coq versions: Coq 8.8 or later
+- License: [BSD 2-Clause "Simplified" License](LICENSE)
+- Compatible Coq versions: Coq 8.11 or later or 8.9
 - Additional dependencies: none
 - Coq namespace: `ExtLib`
 - Related publication(s): none
@@ -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/_CoqProject b/_CoqProject
index d2e4df6a..2a99d756 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -121,7 +121,6 @@ theories/Data/Monads/FuelMonad.v
 theories/Data/Monads/IdentityMonadLaws.v
 theories/Data/Monads/IdentityMonad.v
 theories/Data/Monads/IStateMonad.v
-theories/Data/Monads/ListMonad.v
 theories/Data/Monads/OptionMonadLaws.v
 theories/Data/Monads/OptionMonad.v
 theories/Data/Monads/ReaderMonadLaws.v
diff --git a/coq-ext-lib.opam b/coq-ext-lib.opam
index 07ef44a0..39257a06 100644
--- a/coq-ext-lib.opam
+++ b/coq-ext-lib.opam
@@ -1,29 +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"
-build: [
-  [make "-j%{jobs}%" "theories"]
-]
-run-test: [
-  [make "-j%{jobs}%" "examples"]
-]
-install: [
-  [make "install"]
-]
-depends: [
-  "ocaml"
-  "coq" {>= "8.8"}
-]
+license: "BSD-2-Clause"
+
 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/coqdocjs b/coqdocjs
index 556b3ab2..57401849 160000
--- a/coqdocjs
+++ b/coqdocjs
@@ -1 +1 @@
-Subproject commit 556b3ab2a3199237cde937fe8ac196cf76099eb8
+Subproject commit 57401849fffb24500c078973a8382dd3086fd2bf
diff --git a/examples/ConsiderDemo.v b/examples/ConsiderDemo.v
index ef9f98d7..542a935d 100644
--- a/examples/ConsiderDemo.v
+++ b/examples/ConsiderDemo.v
@@ -1,30 +1,30 @@
 Require Import Coq.Bool.Bool.
-Require NPeano.
-Import NPeano.Nat.
+Require Import Arith.PeanoNat.
 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.
 
 (**  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. omega.
+  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.
-    exfalso; omega.
+    intros. consider (Nat.ltb x y); consider (Nat.ltb y z); consider (Nat.ltb x z); intros; auto.
+    exfalso; lia.
   Qed.
 
 End test.
diff --git a/examples/StateTMonad.v b/examples/StateTMonad.v
new file mode 100644
index 00000000..11b905b1
--- /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 *)
+#[global] 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/meta.yml b/meta.yml
index f5dd5daa..038a8ff2 100644
--- a/meta.yml
+++ b/meta.yml
@@ -4,9 +4,8 @@ shortname: coq-ext-lib
 opam_name: coq-ext-lib
 organization: coq-community
 community: true
-circleci: true
+action: true
 ci_test_dependants: true
-ci_extra_dev: true
 submodule: true
 
 synopsis: A library of Coq definitions, theorems, and tactics
@@ -25,25 +24,54 @@ maintainers:
 opam-file-maintainer: "gmalecha@gmail.com"
 
 license:
-  fullname: The FreeBSD Copyright
-  identifier: BSD
+  fullname: BSD 2-Clause "Simplified" 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.8'
   - version: '8.9'
-  - version: '8.10'
   - version: '8.11'
   - version: '8.12'
   - version: '8.13'
+  - version: '8.14'
+  - version: '8.15'
+  - version: '8.16'
+  - version: '8.17'
+  - version: '8.18'
   - version: 'dev'
 
 make_target: theories
+test_target: examples
 namespace: ExtLib
 
+action_appendix: |2-
+              set -o pipefail  # recommended if the script uses pipes
+
+              startGroup "Generate Coqdoc"
+                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
+            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
   -----
@@ -66,6 +94,12 @@ 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)
+  - [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
diff --git a/theories/Core/Any.v b/theories/Core/Any.v
index 299120b4..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 := {}.
 
@@ -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/Char.v b/theories/Data/Char.v
index 29308938..b144b0de 100644
--- a/theories/Data/Char.v
+++ b/theories/Data/Char.v
@@ -6,50 +6,17 @@ Require Import ExtLib.Core.RelDec.
 Set Implicit Arguments.
 Set Strict Implicit.
 
-Definition 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.
-
-Theorem 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.
-
 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/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/HList.v b/theories/Data/HList.v
index f6e49971..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.
@@ -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. }
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/ListFirstnSkipn.v b/theories/Data/ListFirstnSkipn.v
index 4bd3321d..33d95cc8 100644
--- a/theories/Data/ListFirstnSkipn.v
+++ b/theories/Data/ListFirstnSkipn.v
@@ -1,13 +1,17 @@
 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.
 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 +19,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 +28,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 +44,20 @@ 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.
+#[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),
   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 +65,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 +81,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 +90,9 @@ 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.
+#[global]
+Hint Rewrite skipn_app_L skipn_app_R skipn_0 skipn_all skipn_cons using lia : list_rw.
diff --git a/theories/Data/ListNth.v b/theories/Data/ListNth.v
index 4c05df36..a4a7c0f4 100644
--- a/theories/Data/ListNth.v
+++ b/theories/Data/ListNth.v
@@ -1,4 +1,5 @@
 Require Import Coq.Lists.List.
+Require Import Coq.Arith.PeanoNat.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -13,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,
@@ -22,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,
@@ -44,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.
 
@@ -60,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,
@@ -71,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/Map/FMapAList.v b/theories/Data/Map/FMapAList.v
index c0f1fabd..47c0bc41 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
+*)
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).
diff --git a/theories/Data/Monads/ListMonad.v b/theories/Data/Monads/ListMonad.v
deleted file mode 100644
index dfdd2e85..00000000
--- a/theories/Data/Monads/ListMonad.v
+++ /dev/null
@@ -1,21 +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 _ _ => fix recur c1 c2 :=
-  match c1 with
-    | nil => nil
-    | a :: b => c2 a ++ recur b c2
-  end
-}.
-
-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
-}.
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.
 
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 =>
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/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/Data/String.v b/theories/Data/String.v
index 7d4b32c1..954a956c 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.
@@ -18,7 +17,7 @@ Local Notation "x >> y" := (match x with
                               | z => z
                             end) (only parsing, at level 30).
 
-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
@@ -26,7 +25,10 @@ Definition bool_cmp (l r : bool) : comparison :=
     | false , false => Eq
   end.
 
-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 =>
@@ -34,46 +36,34 @@ 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.
 
-Fixpoint 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
-      else false
-    | _ , _ => false
-  end.
-
-Theorem 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.
-Qed.
+#[deprecated(since="8.15",note="Use Ascii.compare instead.")]
+Notation ascii_cmp := deprecated_ascii_cmp.
 
 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.
 
-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.
@@ -84,19 +74,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/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/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.
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/Programming/Show.v b/theories/Programming/Show.v
index 76807b6e..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.
-    inversion H; 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 }.
diff --git a/theories/Structures/Monad.v b/theories/Structures/Monad.v
index bab11714..2b500330 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.
 
@@ -83,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.
 
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)
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.