From 13da286727221ffdc5b43515aa62df85e3f28160 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 13 May 2022 11:54:31 +0200
Subject: [PATCH] Set `Hint Mode` for `FinSet`.

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

diff --git a/theories/base.v b/theories/base.v
index a09cd676..f8105fb3 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1468,6 +1468,8 @@ Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
   elem_of_elements (X : C) x : x ∈ elements X ↔ x ∈ X;
   NoDup_elements (X : C) : NoDup (elements X)
 }.
+Global Hint Mode FinSet - ! - - - - - - - - : typeclass_instances.
+
 Class Size C := size: C → nat.
 Global Hint Mode Size ! : typeclass_instances.
 Global Arguments size {_ _} !_ / : simpl nomatch, assert.
-- 
GitLab