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

[helm.git] / helm / matita / library / Z / plus.ma

diff --git a/helm/matita/library/Z/plus.ma b/helm/matita/library/Z/plus.ma
index dc743e60bc77f384ecdadd927cee18d5ae085461..b89f291fbb918684cb595dbd54b5d423259e7e23 100644 (file)
--- a/helm/matita/library/Z/plus.ma
+++ b/helm/matita/library/Z/plus.ma
@@ -59,12 +59,12 @@ simplify.
 rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
 simplify.
 rewrite > nat_compare_n_m_m_n.
-simplify.elim nat_compare ? ?.simplify.reflexivity.
+simplify.elim nat_compare.simplify.reflexivity.
 simplify. reflexivity.
 simplify. reflexivity.
 elim y.simplify.reflexivity.
 simplify.rewrite > nat_compare_n_m_m_n.
-simplify.elim nat_compare ? ?.simplify.reflexivity.
+simplify.elim nat_compare.simplify.reflexivity.
 simplify. reflexivity.
 simplify. reflexivity.
 simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.