From a03c40c5862353e0e9b6e8d29b3664acbc3e4afa Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 30 Nov 2021 12:27:25 -0500
Subject: [PATCH] make use of bidirectionality hint for tele_app

---
 CHANGELOG.md          | 2 ++
 theories/telescopes.v | 4 +++-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ae9279fe..1c832122 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 c02e9c5e..8c71582e 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. *)
-- 
GitLab