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.