X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcore_notation.moo;h=ed0c7007beb4e5384bf19097347e689bef0e4c17;hb=0b15dfdee3357a626c77d30599e87a83ab34e471;hp=0043825ceaf32df56b2921c88074abb7b7ac1e3b;hpb=2bd1dbc6fdad64f989089165a4e7367c072d2656;p=helm.git

diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index 0043825ce..ed0c7007b 100644
--- a/helm/software/matita/core_notation.moo
+++ b/helm/software/matita/core_notation.moo
@@ -4,7 +4,6 @@ for @{ 'exists ${default
   @{\lambda ${ident i} : $ty. $p}
   @{\lambda ${ident i} . $p}}}.
 
-(* Bugged notation: $T is not used if provided *)
 notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
   with precedence 20
   for ${ default