X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsetoids1.ma;h=85038ab1694a89e2a40a27d8331aaad88f7e3f5f;hb=8b1a49bbee9eea86eb74c040defe701370ca5893;hp=bae7f549ecc5ca3fdf800b59788aa5b3eaf48399;hpb=6678a28314d8878bb46d5de7b1060628f4930242;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).