New version of the library. Several files still do not compile.

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

diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma
index 69a9ff20bb115c5521977c4bab6d7d46f53a5ffd..3211814db099d89326c46bbc9dfb6d5cde551f21 100644 (file)
--- a/matita/matita/lib/arithmetics/bigops.ma
+++ b/matita/matita/lib/arithmetics/bigops.ma
@@ -265,7 +265,7 @@ theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2.
   ]
 qed.
 
-(* Sigma e Pi - da generalizzare *)
+(* Sigma e Pi *)
 notation "Σ_{ ident i < n | p } f"
   with precedence 80
 for @{'bigop $n plus 0 (λ${ident i}.p) (λ${ident i}. $f)}.