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/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. *)