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

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

diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma
index a3a71522804d7eee69c2f5461d3fd7fe79d73fbf..4628eca13c1d86f1f545f95784b118f814b4832b 100644 (file)
--- a/helm/matita/library/nat/factorization.ma
+++ b/helm/matita/library/nat/factorization.ma
@@ -216,7 +216,7 @@ elim Hcut2.absurd O=r.
 apply le_n_O_to_eq.apply le_S_S_to_le.exact H5.
 simplify.intro.
 cut O=n1.
-apply not_le_Sn_O O ?.
+apply not_le_Sn_O O.
 rewrite > Hcut3 in \vdash (? ? %).
 assumption.rewrite > Hcut. 
 rewrite < H6.reflexivity.
@@ -273,7 +273,7 @@ cut (S(S m1)) = r.
 rewrite > Hcut3 in \vdash (? (? ? %)).
 change with divides (nth_prime p) r \to False.
 intro.
-apply plog_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r ? ? ? ?.
+apply plog_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r.
 apply lt_SO_nth_prime_n.
 simplify.apply le_S_S.apply le_O_n.apply le_n.
 assumption.
@@ -301,7 +301,7 @@ cut r \lt (S O) \or r=(S O).
 elim Hcut3.absurd O=r.
 apply le_n_O_to_eq.apply le_S_S_to_le.exact H2.
 simplify.intro.
-apply not_le_Sn_O O ?.
+apply not_le_Sn_O O.
 rewrite > H3 in \vdash (? ? %).assumption.assumption.
 apply le_to_or_lt_eq r (S O).
 apply not_lt_to_le.assumption.
@@ -400,7 +400,7 @@ intro.
 cut i = j.
 apply not_le_Sn_n i.rewrite > Hcut1 in \vdash (? ? %).assumption.
 apply injective_nth_prime ? ? H4.
-apply H i (S j) ?.
+apply H i (S j).
 apply trans_lt ? j.assumption.simplify.apply le_n.
 assumption.
 apply divides_times_to_divides.
@@ -470,7 +470,7 @@ simplify in H4.
 rewrite > plus_n_O.
 rewrite > plus_n_O (defactorize_aux n3 (S i)).assumption.
 apply False_ind.
-apply not_divides_defactorize_aux n1 i (S i) ?.
+apply not_divides_defactorize_aux n1 i (S i).
 simplify. apply le_n.
 simplify in H5.
 rewrite > plus_n_O (defactorize_aux n1 (S i)).
@@ -480,7 +480,7 @@ apply witness ? ? ((exp (nth_prime i) n5)*(defactorize_aux n3 (S i))).
 reflexivity.
 intros.
 apply False_ind.
-apply not_divides_defactorize_aux n3 i (S i) ?.
+apply not_divides_defactorize_aux n3 i (S i).
 simplify. apply le_n.
 simplify in H4.
 rewrite > plus_n_O (defactorize_aux n3 (S i)).