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

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

diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 37c60b4057713ac77ddf68e638b2279db7f235a9..0b8f2bbe207f38580c466e45152f7cffc88cbbb2 100644 (file)
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -43,7 +43,7 @@ n < smallest_factor (S (fact n)).
 intros.
 apply not_le_to_lt.
 change with smallest_factor (S (fact n)) \le n \to False.intro.
-apply not_divides_S_fact n (smallest_factor(S (fact n))) ? ?.
+apply not_divides_S_fact n (smallest_factor(S (fact n))).
 apply lt_SO_smallest_factor.
 simplify.apply le_S_S.apply le_SO_fact.
 assumption.