From 3303ec5e5ba14c5abdcb17ca5f99fe024434f40d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 4 Sep 2021 22:45:53 -0400
Subject: [PATCH] make name more consistent

---
 theories/fin_map_dom.v | 2 +-
 theories/fin_sets.v    | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 75aeb309..4d9d66ef 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -177,7 +177,7 @@ Qed.
 Lemma size_dom `{!Elements K D, !FinSet K D} {A} (m : M A) :
   size (dom D m) = size m.
 Proof.
-  rewrite dom_alt, list_to_set_size.
+  rewrite dom_alt, size_list_to_set.
   2:{ apply NoDup_fst_map_to_list. }
   unfold size, map_size. rewrite fmap_length. done.
 Qed.
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 0f81651d..14aef32f 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -203,7 +203,7 @@ Proof.
   by apply size_non_empty_iff, non_empty_difference.
 Qed.
 
-Lemma list_to_set_size l :
+Lemma size_list_to_set l :
   NoDup l → size (list_to_set (C:=C) l) = length l.
 Proof.
   intros Hl. unfold size, set_size. simpl.
-- 
GitLab