From b16e3e3cfc62ff171932938aa896191eae29c3df Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 12 Dec 2018 16:19:58 +0100
Subject: [PATCH] =?UTF-8?q?Notation=20`=E2=89=A1{n}@{A}=E2=89=A1`=20to=20b?=
 =?UTF-8?q?e=20explicit=20about=20the=20type=20in=20`=E2=89=A1{n}=E2=89=A1?=
 =?UTF-8?q?`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/algebra/ofe.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index facbfd82b..3c095092e 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -16,6 +16,9 @@ Class Dist A := dist : nat → relation A.
 Instance: Params (@dist) 3.
 Notation "x ≡{ n }≡ y" := (dist n x y)
   (at level 70, n at next level, format "x  ≡{ n }≡  y").
+Notation "x ≡{ n }@{ A }≡ y" := (dist (A:=A) n x y)
+  (at level 70, n at next level, only parsing).
+
 Hint Extern 0 (_ ≡{_}≡ _) => reflexivity : core.
 Hint Extern 0 (_ ≡{_}≡ _) => symmetry; assumption : core.
 Notation NonExpansive f := (∀ n, Proper (dist n ==> dist n) f).
-- 
GitLab