X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Frelations.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Frelations.ma;h=307797566dce8ea8280697246208f44e943a6fbf;hb=0080faad4e730c227b6bbb2549407b23703b477a;hp=74a7c7d7839bb26fee44529654fc3cc5ff653bb2;hpb=5ab72ef7c6da38f9bc239e13f049521922987183;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
index 74a7c7d78..307797566 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
@@ -98,10 +98,8 @@ definition REL: category1.
           first [apply refl | assumption]]]
 qed.
 
-(* 
 definition setoid_of_REL : objs1 REL → setoid ≝ λx.x.
 coercion setoid_of_REL.
-*)
 
 definition binary_relation_setoid_of_arrow1_REL : 
   ∀P,Q. arrows1 REL P Q → binary_relation_setoid P Q ≝ λP,Q,x.x.