From 9a5be071907d072d31e9759db3b64a7bab174eed Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 4 Dec 2017 23:14:36 +0100
Subject: [PATCH] sqsubseteq is a RewriteRelation.

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

diff --git a/theories/base.v b/theories/base.v
index 2573b63..532e746 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1125,6 +1125,7 @@ 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.
+Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑).
 
 Class Meet A := meet: A → A → A.
 Hint Mode Meet ! : typeclass_instances.
-- 
GitLab