From: Claudio Sacerdoti Coen Date: Mon, 12 Dec 2011 16:35:41 +0000 (+0000) Subject: Parentheses are now needed. I do not know why and when this has changed. X-Git-Tag: make_still_working~2026 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=da5cf21f33e7303bf9b1fc60470de1f6101714dd;p=helm.git Parentheses are now needed. I do not know why and when this has changed. --- diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma index 7c5df29f3..c8b2a25bf 100644 --- a/matita/matita/lib/arithmetics/primes.ma +++ b/matita/matita/lib/arithmetics/primes.ma @@ -439,9 +439,9 @@ let rec nth_prime n ≝ match n with min upper_bound (S previous_prime) primeb]. lemma nth_primeS: ∀n.nth_prime (S n) = - let previous_prime ≝ nth_prime n in + (let previous_prime ≝ nth_prime n in let upper_bound ≝ S previous_prime! in - min upper_bound (S previous_prime) primeb. + min upper_bound (S previous_prime) primeb). // qed. (* it works *)