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

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

diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma
index 443c6657f9085642d307a9f1b123a22546e11074..22c8b25a790d1551df8d23d55847352e9eb9f9b6 100644 (file)
--- a/helm/matita/library/nat/compare.ma
+++ b/helm/matita/library/nat/compare.ma
@@ -43,7 +43,7 @@ simplify.reflexivity.
 simplify.apply not_eq_O_S.
 intro.
 simplify.
-intro. apply not_eq_O_S n1 ?.apply sym_eq.assumption.
+intro. apply not_eq_O_S n1.apply sym_eq.assumption.
 intros.simplify.
 generalize in match H.
 elim (eqb n1 m1).