Setoid rewriting as unification hinting. Does not work recursively yet.

[helm.git] / helm / software / matita / nlibrary / sets / setoids1.ma

diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma
index bae7f549ecc5ca3fdf800b59788aa5b3eaf48399..85038ab1694a89e2a40a27d8331aaad88f7e3f5f 100644 (file)
--- 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).