X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Flogic%2Fconnectives.ma;h=832d1a531fee7a18ee64c1de57997af27a867f15;hb=916c558005ed665c62699a7a4c5347870c8a3efb;hp=6a20bc8979c15805f2be51269218e05c3015eb20;hpb=eff920e57112c3eaee889384d435602e41951a36;p=helm.git

diff --git a/helm/software/matita/library/logic/connectives.ma b/helm/software/matita/library/logic/connectives.ma
index 6a20bc897..832d1a531 100644
--- a/helm/software/matita/library/logic/connectives.ma
+++ b/helm/software/matita/library/logic/connectives.ma
@@ -49,7 +49,6 @@ inductive Or (A,B:Prop) : Prop \def
      or_introl : A \to (Or A B)
    | or_intror : B \to (Or A B).
 
-(*CSC: the URI must disappear: there is a bug now *)
 interpretation "logical or" 'or x y = (Or x y).
 
 theorem Or_ind':