From ca6ea63a7a04b08fa5d859388ba5e8943d3d2351 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 5 Apr 2018 11:30:40 +0200
Subject: [PATCH] =?UTF-8?q?Notation=20`=E2=8A=91@{A}`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/base.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index 571ac7d7..b229cba6 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1204,6 +1204,10 @@ Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
 Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
 Notation "( x ⊑)" := (sqsubseteq x) (only parsing) : stdpp_scope.
 Notation "(⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
+
+Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
+Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
+
 Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑).
 
 Hint Extern 0 (_ ⊑ _) => reflexivity.
-- 
GitLab