From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 15 Jul 2008 09:09:30 +0000 (+0000)
Subject: removed dummy comment
X-Git-Tag: make_still_working~4930
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fa3ef782b1336310a78868e7dfc900fa988ee2ab;p=helm.git

removed dummy comment
---

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