Removed final question marks from {apply|elim|rewrite}s.

[helm.git] / helm / matita / library / nat / nat.ma

diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index 100cb0f0356afccc78a3b06f8c2c7e62da4953a0..aae6434e7e55657890c883550dc380d2db86275f 100644 (file)
--- 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.