Parentheses are now needed. I do not know why and when this has changed.

[helm.git] / matita / matita / lib / arithmetics / primes.ma

diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma
index 7c5df29f35151cebe5d3c6664368c8ee9f2ece73..c8b2a25bf4e5f9d05ac3fffc2b0305c9a23ae66a 100644 (file)
--- 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 *)