From e315714546715fe72d5dbc10fdd5b91ad7e1efc5 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 5 Oct 2021 14:14:09 +0200
Subject: [PATCH] Mark set_size and set_fold as TC opaque

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

diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 9696381f..e9afdfb0 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -10,9 +10,11 @@ Set Default Proof Using "Type*".
 
 (** Operations *)
 Global Instance set_size `{Elements A C} : Size C := length ∘ elements.
+Typeclasses Opaque set_size.
 
 Definition set_fold `{Elements A C} {B}
   (f : A → B → B) (b : B) : C → B := foldr f b ∘ elements.
+Typeclasses Opaque set_fold.
 
 Global Instance set_filter
     `{Elements A C, Empty C, Singleton A C, Union C} : Filter A C := λ P _ X,
-- 
GitLab