X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsetoids1.ma;h=85038ab1694a89e2a40a27d8331aaad88f7e3f5f;hb=835f6498543d1f20cb02d134c1b22be7d622420e;hp=bae7f549ecc5ca3fdf800b59788aa5b3eaf48399;hpb=0af747f54642b05b3232319b6ae1753af211dba5;p=helm.git

diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma
index bae7f549e..85038ab16 100644
--- a/helm/software/matita/nlibrary/sets/setoids1.ma
+++ b/helm/software/matita/nlibrary/sets/setoids1.ma
@@ -30,8 +30,8 @@ ndefinition setoid1_of_setoid: setoid → setoid1.
     | napply trans]##]
 nqed.
 
-ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid
- on _s: setoid to setoid1.
+(*ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid
+ on _s: setoid to setoid1.*)
 (*prefer coercion Type_OF_setoid.*)
 
 interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y).