From 397132917385d7282a0bfe4deefe57ceacb71cc9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 29 Oct 2020 09:42:33 +0100
Subject: [PATCH] fix build on old Coq

---
 theories/sets.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/sets.v b/theories/sets.v
index 14005f60..5e1e72d6 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -882,11 +882,11 @@ Section fin_to_set.
   Context `{SemiSet A C, Finite A}.
   Implicit Types a : A.
 
-  Lemma elem_of_fin_to_set a : a ∈ fin_to_set A.
+  Lemma elem_of_fin_to_set a : a ∈@{C} fin_to_set A.
   Proof. apply elem_of_list_to_set, elem_of_enum. Qed.
 
   Global Instance set_unfold_fin_to_set a :
-    SetUnfoldElemOf a (fin_to_set A) True.
+    SetUnfoldElemOf (C:=C) a (fin_to_set A) True.
   Proof. constructor. split; auto using elem_of_fin_to_set. Qed.
 End fin_to_set.
 
-- 
GitLab