X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Flist%2Flist.ma;h=9ecfd50e3ff41bf5cf89e6604ea2ca4986cf7e48;hb=2f93bd3b7db5527fd5a61da093e16b0f26484695;hp=bb341d245fad82a43657e4e427956968fac8b3c2;hpb=b2788a5ed06fa093c607ea3f5a29058845e1f9c6;p=helm.git

diff --git a/matita/library/list/list.ma b/matita/library/list/list.ma
index bb341d245..9ecfd50e3 100644
--- a/matita/library/list/list.ma
+++ b/matita/library/list/list.ma
@@ -44,7 +44,7 @@ theorem nil_cons:
   intros;
   unfold Not;
   intros;
-  discriminate H.
+  destruct H.
 qed.
 
 let rec id_list A (l: list A) on l :=