From 03966a39f4828cab8ea4b365a6347f83197fbddd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 10 Jan 2018 08:09:57 -0800
Subject: [PATCH] =?UTF-8?q?`reflexivity`=20hint=20for=20`=5F=20=E2=8A=91?=
 =?UTF-8?q?=20=5F`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

As we have for all classes for binary relations.
---
 theories/base.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index 763e86c4..61d2b69a 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1138,6 +1138,8 @@ Notation "( x ⊑)" := (sqsubseteq x) (only parsing) : stdpp_scope.
 Notation "(⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
 Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑).
 
+Hint Extern 0 (_ ⊑ _) => reflexivity.
+
 Class Meet A := meet: A → A → A.
 Hint Mode Meet ! : typeclass_instances.
 Instance: Params (@meet) 2.
-- 
GitLab