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.