]> matita.cs.unibo.it Git - helm.git/commitdiff
removed dummy comment
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 15 Jul 2008 09:09:30 +0000 (09:09 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 15 Jul 2008 09:09:30 +0000 (09:09 +0000)
helm/software/matita/core_notation.moo

index 0043825ceaf32df56b2921c88074abb7b7ac1e3b..ed0c7007beb4e5384bf19097347e689bef0e4c17 100644 (file)
@@ -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