From 6dcccf0604added2ce749ca1616abd3f6b8d1a95 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Glen=20M=C3=A9vel?= <glen.mevel@inria.fr>
Date: Tue, 21 Dec 2021 17:03:22 +0100
Subject: [PATCH] add comment about Qed/Defined for `finite_sig_dec`

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

diff --git a/theories/finite.v b/theories/finite.v
index 9bde7e87..b2fa877e 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -382,7 +382,7 @@ Proof.
     - apply elem_of_list_fmap_1_alt with (x ↾ Hx); [apply elem_of_enum|]; done.
     - apply elem_of_list_fmap in Hx as [[x' Hx'] [-> _]]; done. }
   destruct (decide (x ∈ xs)); [left | right]; naive_solver.
-Qed.
+Qed. (* <- could be Defined but this lemma will probably not be used for computing *)
 
 Section sig_finite.
   Context {A} (P : A → Prop) `{∀ x, Decision (P x)}.
-- 
GitLab