Procedural: we corrected two errors about the handling of mutcase (the "cases"

[helm.git] / helm / software / matita / library / logic / connectives.ma

diff --git a/helm/software/matita/library/logic/connectives.ma b/helm/software/matita/library/logic/connectives.ma
index 6a20bc8979c15805f2be51269218e05c3015eb20..832d1a531fee7a18ee64c1de57997af27a867f15 100644 (file)
--- 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':