From 50364a0e2514450e1dd50087e853374031600270 Mon Sep 17 00:00:00 2001
From: Valerii Huhnin <olympichek1@gmail.com>
Date: Mon, 31 Mar 2025 10:52:18 +0300
Subject: [PATCH] define `NoDup_dec` with `Defined` instead of `Qed`

---
 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..80420d944b 100644
--- a/theories/Lists/ListDec.v
+++ b/theories/Lists/ListDec.v
@@ -95,7 +95,7 @@ Proof using A dec.
    + destruct IH.
      * left. now constructor.
      * right. inversion_clear 1. tauto.
-Qed.
+Defined.
 
 End Dec_in_Type.