diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 948a98f18cf14feb75eff25c52dcfd67b1087f3f..dd67e296cd04726f326d043d9e21285ec7352b08 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -77,14 +77,8 @@ build-coq.8.12.2:
     DENY_WARNINGS: "1"
 
 build-coq.8.11.2:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.11.2"
-    DENY_WARNINGS: "1"
-
-build-coq.8.10.2:
   <<: *template
   <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.10.2"
+    OPAM_PINS: "coq version 8.11.2"
     DENY_WARNINGS: "1"
diff --git a/CHANGELOG.md b/CHANGELOG.md
index ae9279fe47c0ac36421ef5fd8e81c714fa68cac3..1c832122bd051329ff77e31600ea9d9d8ecaf0b4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,8 @@ API-breaking change is listed.
 
 ## std++ master
 
+Coq 8.10 is no longer supported by this release.
+
 - Add `list.zip_with_take_both` and `list.zip_with_take_both'`
 - Specialize `list.zip_with_take_{l,r}`, add generalized lemmas `list.zip_with_take_{l,r}'`
 - Add `bool_to_Z` that converts true to 1 and false to 0. (by Michael Sammler)
diff --git a/README.md b/README.md
index eeb23fba9d207bc185d07baea46f121f2264d4cf..be93cd60a1b4f39b31a97d74c15fdd27f1333f05 100644
--- a/README.md
+++ b/README.md
@@ -45,7 +45,7 @@ Notably:
 
 This version is known to compile with:
 
- - Coq version 8.10.2 / 8.11.2 / 8.12.2 / 8.13.2 / 8.14.1
+ - Coq version 8.11.2 / 8.12.2 / 8.13.2 / 8.14.1
 
 ## Installing via opam
 
diff --git a/coq-stdpp.opam b/coq-stdpp.opam
index 67872a065c70ef50536c8479cbac46bd5033beb2..1e5f8d626ef442df7e03ee132337e03c85e6ac82 100644
--- a/coq-stdpp.opam
+++ b/coq-stdpp.opam
@@ -33,7 +33,7 @@ tags: [
 ]
 
 depends: [
-  "coq" { (>= "8.10.2" & < "8.15~") | (= "dev") }
+  "coq" { (>= "8.11" & < "8.15~") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/tests/telescopes.ref b/tests/telescopes.ref
index afac10f0b0fddd77cc435c1097c467da2a88d1fb..2c58e6389dcd6063da7a3f15a26d2863bc62b4f6 100644
--- a/tests/telescopes.ref
+++ b/tests/telescopes.ref
@@ -18,3 +18,5 @@
   HÎ³ : Î³1 x
   ============================
   Î³1 x âˆ¨ Î³2 x
+[TEST x y : nat, x = y]
+     : Prop
diff --git a/tests/telescopes.v b/tests/telescopes.v
index 56633586fa2e6089fa9e591c61b2a8f505e48c4f..260b7283cbcda1dc77a908295c7d6e939293adf9 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -31,3 +31,13 @@ Proof.
 Qed.
 End tests.
 End accessor.
+
+(* Type inference for tele_app-based notation.
+(Relies on [&] bidirectionality hint of tele_app.) *)
+Definition test {TT : tele} (t : TT â†’ Prop) : Prop :=
+  âˆ€.. x, t x âˆ§ t x.
+Notation "'[TEST'  x .. z ,  P ']'" :=
+  (test (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..)))
+        (tele_app (Î» x, .. (Î» z, P) ..)))
+  (x binder, z binder).
+Check [TEST (x y : nat), x = y].
diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 5eab4ad96aae2865bd98a65baff874fd10e46ec3..6935137074870c2079f54f118e732bc618a1c24a 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -321,12 +321,11 @@ Section Z_little_endian.
       rewrite orb_false_l. f_equal. lia.
   Qed.
 
-  (* TODO: replace the calls to [nia] by [lia] after dropping support for Coq 8.10.2. *)
   Lemma little_endian_to_Z_to_little_endian m n z:
     0 â‰¤ n â†’ 0 â‰¤ m â†’
     little_endian_to_Z n (Z_to_little_endian m n z) = z `mod` 2 ^ (m * n).
   Proof.
-    intros ? Hm. rewrite <-Z.land_ones by nia.
+    intros ? Hm. rewrite <-Z.land_ones by lia.
     revert z.
     induction m as [|m ? IH|] using (Z_succ_pred_induction 0); intros z; [..|lia].
     { Z.bitwise. by rewrite andb_false_r. }
@@ -335,10 +334,10 @@ Section Z_little_endian.
     rewrite Z.land_spec, Z.lor_spec, Z.shiftl_spec, !Z.land_spec by lia.
     rewrite (Z_ones_spec n z') by lia. case_bool_decide.
     - rewrite andb_true_r, (Z.testbit_neg_r _ (z' - n)), orb_false_r by lia. simpl.
-      by rewrite Z_ones_spec, bool_decide_true, andb_true_r by nia.
+      by rewrite Z_ones_spec, bool_decide_true, andb_true_r by lia.
     - rewrite andb_false_r, orb_false_l.
       rewrite Z.shiftr_spec by lia. f_equal; [f_equal; lia|].
-      rewrite !Z_ones_spec by nia. apply bool_decide_iff. lia.
+      rewrite !Z_ones_spec by lia. apply bool_decide_iff. lia.
   Qed.
 
   Lemma Z_to_little_endian_length m n z :
@@ -368,11 +367,11 @@ Section Z_little_endian.
     0 â‰¤ little_endian_to_Z n bs < 2 ^ (Z.of_nat (length bs) * n).
   Proof.
     intros ?. induction 1 as [|b bs Hb ? IH]; [done|]; simpl.
-    apply Z_bounded_iff_bits_nonneg'; [nia|..].
+    apply Z_bounded_iff_bits_nonneg'; [lia|..].
     { apply Z.lor_nonneg. split; [lia|]. apply Z.shiftl_nonneg. lia. }
     intros z' ?. rewrite Z.lor_spec.
     rewrite Z_bounded_iff_bits_nonneg' in Hb by lia.
-    rewrite Hb, orb_false_l, Z.shiftl_spec by nia.
-    apply (Z_bounded_iff_bits_nonneg' (Z.of_nat (length bs) * n)); nia.
+    rewrite Hb, orb_false_l, Z.shiftl_spec by lia.
+    apply (Z_bounded_iff_bits_nonneg' (Z.of_nat (length bs) * n)); lia.
   Qed.
 End Z_little_endian.
diff --git a/theories/telescopes.v b/theories/telescopes.v
index c02e9c5ecccc6af21c91ab7ad84e683e027cfdfd..8c71582ec48d08cd4c85e0701925428e87b5ea17 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -45,7 +45,9 @@ Definition tele_app {TT : tele} {T} (f : TT -t> T) : tele_arg TT â†’ T :=
      | TargO => Î» t : T, t
      | TargS x a => Î» f, rec a (f x)
      end) TT a f.
-Global Arguments tele_app {!_ _} _ !_ /.
+(* The bidirectionality hint [&] simplifies defining tele_app-based notation
+such as the atomic updates and atomic triples in Iris. *)
+Global Arguments tele_app {!_ _} & _ !_ /.
 
 Coercion tele_arg : tele >-> Sortclass.
 (* This is a local coercion because otherwise, the "Î».." notation stops working. *)