* Obsolete debugging comments removed

[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 8035d49ddba64dcb5d207ab2e4c9179d477d4d2c..200ccba5a9086b0ca2a940c7f19ae0964bb8402c 100644 (file)
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -62,7 +62,7 @@ apply ex_intro nat ? (smallest_factor (S (fact (S n1)))).
 split.split.
 apply smallest_factor_fact.
 apply le_smallest_factor_n.
-(* ancora hint non lo trova *)
+(* Andrea: ancora hint non lo trova *)
 apply prime_smallest_factor_n.
 change with (S(S O)) \le S (fact (S n1)).
 apply le_S.apply le_SSO_fact.
@@ -98,7 +98,6 @@ apply nat_case n.
 change with prime (S(S O)).
 apply primeb_to_Prop (S(S O)).
 intro.
-(* ammirare la resa del letin !! *)
 change with
 let previous_prime \def (nth_prime m) in
 let upper_bound \def S (fact previous_prime) in