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

diff --git a/helm/software/matita/contribs/dama/dama/sequence.ma b/helm/software/matita/contribs/dama/dama/sequence.ma
index c64315481..d3acf437f 100644
--- a/helm/software/matita/contribs/dama/dama/sequence.ma
+++ b/helm/software/matita/contribs/dama/dama/sequence.ma
@@ -22,16 +22,13 @@ definition fun_of_seq: ∀O:Type.sequence O → nat → O ≝
 
 coercion cic:/matita/dama/sequence/fun_of_seq.con 1.
 
-notation < "hvbox((\lfloor p \rfloor) \sub ident i)"
-  left associative with precedence 70
+notation < "hvbox((\lfloor term 19 p \rfloor) \sub ident i)" with precedence 90
 for @{ 'sequence (\lambda ${ident i} : $t . $p)}.
 
-notation > "hvbox((\lfloor p \rfloor) \sub ident i)"
-  left associative with precedence 70
+notation > "hvbox((\lfloor term 19 p \rfloor) \sub ident i)" with precedence 90
 for @{ 'sequence (\lambda ${ident i} . $p)}.
 
-notation > "hvbox(\lfloor ident i, p \rfloor)"
-  left associative with precedence 70
+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