From f5fc5467bbd8b631832d0304724698bef131345e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Wed, 10 Jun 2026 14:35:31 +0200
Subject: [PATCH] Adapt to rocq-prover/rocq#22113 (Proof Using Clear Unused)

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

diff --git a/theories/Lists/ListDec.v b/theories/Lists/ListDec.v
index 3d1638afaa..0eb1ee7db6 100644
--- a/theories/Lists/ListDec.v
+++ b/theories/Lists/ListDec.v
@@ -65,7 +65,7 @@ Qed.
 
 Lemma NoDup_list_decidable (l:list A) : NoDup l -> forall x y:A, In x l -> In y l -> decidable (x=y).
 Proof using A.
-  clear dec; intros Hl; induction Hl; firstorder congruence.
+  try clear dec; intros Hl; induction Hl; firstorder congruence.
 Qed.
 
 End Dec_in_Prop.