From be8dfddb73495cca9b96d0ce186902b734b0eadc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 21 Aug 2013 14:50:55 +0200
Subject: [PATCH] Use wf_projected instead of well_founded_lt_compat

---
 theories/fin_collections.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index f0af0c92..ecccd40b 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -145,7 +145,7 @@ Proof.
 Qed.
 
 Lemma collection_wf : wf (strict (@subseteq C _)).
-Proof. apply well_founded_lt_compat with size, subset_size. Qed.
+Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
 
 Lemma collection_ind (P : C → Prop) :
   Proper ((≡) ==> iff) P →
-- 
GitLab