From 872a4579840171edf6822abc7c79d26b2d0bb9aa Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com> Date: Tue, 5 Oct 2021 14:12:49 +0200 Subject: [PATCH] fin_sets: mark set_fresh TC opaque --- theories/fin_sets.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/fin_sets.v b/theories/fin_sets.v index d53d3e05..d6c7c31a 100644 --- a/theories/fin_sets.v +++ b/theories/fin_sets.v @@ -26,7 +26,7 @@ Typeclasses Opaque set_map. Global Instance set_fresh `{Elements A C, Fresh A (list A)} : Fresh A C := fresh ∘ elements. -Typeclasses Opaque set_filter. +Typeclasses Opaque set_fresh. (** We generalize the [fresh] operation on sets to generate lists of fresh elements w.r.t. a set [X]. *) -- GitLab