X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fnat.ma;h=aae6434e7e55657890c883550dc380d2db86275f;hb=2ecd65dbcc1388bb2dfe6425e6ef1b2e3f45c4ac;hp=100cb0f0356afccc78a3b06f8c2c7e62da4953a0;hpb=5a702cea95883f7095c16b450e065ccb1714fc5a;p=helm.git

diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index 100cb0f03..aae6434e7 100644
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -97,7 +97,7 @@ intro.elim n1.
 left.reflexivity.
 right.apply not_eq_O_S.
 intro.right.intro.
-apply not_eq_O_S n1 ?.
+apply not_eq_O_S n1.
 apply sym_eq.assumption.
 intros.elim H.
 left.apply eq_f. assumption.