`reflexivity` hint for `_ ⊑ _`.

As we have for all classes for binary relations.

`reflexivity` hint for `_ ⊑ _`.
As we have for all classes for binary relations.
03966a39 · Robbert Krebbers · 11b9fbe1 · 03966a39
Commit 03966a39 authored Jan 10, 2018 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 0 deletions

base.v theories/base.v +2 -0

No files found.
--- 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.