aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--theories/ZArith/Zcomplements.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index e49131a4cc..bcf90f9618 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -306,7 +306,7 @@ Unfold Zlength; Intros; Rewrite H; Auto.
Qed.
Implicits Zlength_correct [1].
-Lemma Zlength_nil : (A:Set)(x:A)(l:(list A))(Zlength (nil A))=0.
+Lemma Zlength_nil : (A:Set)(Zlength (nil A))=0.
Proof.
Auto.
Qed.