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

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

diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 3acce20afe21277adfab0b15c6d023022afd5da5..079e902ad39ba9213b28b7b58062ed9e9db39dcb 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -82,7 +82,7 @@ qed.
 
 theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to 
 n = m+p.
-intros.apply trans_eq ? ? ((n-m)+m) ?.
+intros.apply trans_eq ? ? ((n-m)+m).
 apply plus_minus_m_m.
 apply H.elim H1.
 apply sym_plus.
@@ -220,7 +220,7 @@ apply (leb_elim z y).
     apply inj_plus_l (x*z).assumption.
     apply trans_eq nat ? (x*y).
       rewrite < distr_times_plus.rewrite < plus_minus_m_m ? ? H.reflexivity.
-      rewrite < plus_minus_m_m ? ? ?.
+      rewrite < plus_minus_m_m.
         reflexivity.
         apply le_times_r.assumption.
   intro.rewrite > eq_minus_n_m_O.