Downgrades buggy destruct patch.

[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 447cda347a5c0dfe60fdd9dd432521c32e0f7491..97bda394da6d144854b122000456d94146ce0a22 100644 (file)
--- a/matita/matita/lib/arithmetics/bigops.ma
+++ b/matita/matita/lib/arithmetics/bigops.ma
@@ -70,7 +70,7 @@ notation "\big  [ op , nil ]_{ ident j ∈ [a,b[ } f"
 for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.  
  
-(* notation "\big  [ op , nil ]_{( term 50) a ≤ ident j < b | p } f"
+(* notation "\big  [ op , nil ]_{( term 55) a ≤ ident j < b | p } f"
   with precedence 80
 for @{\big[$op,$nil]_{${ident j} < ($b-$a) | ((λ${ident j}.$p) (${ident j}+$a))}((λ${ident j}.$f)(${ident j}+$a))}.
 *)