X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Flist%2Flist.ma;h=9ecfd50e3ff41bf5cf89e6604ea2ca4986cf7e48;hb=576a1f3f67dc0207a664a127fe482facbfa2a826;hp=bb341d245fad82a43657e4e427956968fac8b3c2;hpb=64afac782fe3bd83dbc2f9295481362f1edc8e68;p=helm.git

diff --git a/helm/software/matita/library/list/list.ma b/helm/software/matita/library/list/list.ma
index bb341d245..9ecfd50e3 100644
--- a/helm/software/matita/library/list/list.ma
+++ b/helm/software/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 :=