X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fsequence.ma;h=948d14f67963ef2e929bba924e40edbe58572ea4;hb=21f1fb39b5e1187ef87387f20522e60abe4f7c19;hp=d3acf437ff68684cc089044582fd29c1ad81800e;hpb=25aa80d913c903fcc270d05464cf3084b12d52a8;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/sequence.ma b/helm/software/matita/contribs/dama/dama/sequence.ma
index d3acf437f..948d14f67 100644
--- a/helm/software/matita/contribs/dama/dama/sequence.ma
+++ b/helm/software/matita/contribs/dama/dama/sequence.ma
@@ -31,7 +31,7 @@ for @{ 'sequence (\lambda ${ident i} . $p)}.
 notation > "hvbox(\lfloor ident i, term 19 p \rfloor)" with precedence 90
 for @{ 'sequence (\lambda ${ident i} . $p)}.
   
-notation "a \sub i" left associative with precedence 70 
+notation "a \sub i" left associative with precedence 90 
   for @{ 'sequence_appl $a $i }.
 
 interpretation "sequence" 'sequence \eta.x = (mk_seq _ x).