X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fcategories.ma;h=e22402d9f52542745b29e226597fe74a14920622;hb=79eedc2380427ff60d61c8de32ac7cecf3d4f08b;hp=84cde74dddc6ec669e2c8ee68232104e186c4d95;hpb=7db606e36d5c17681a62cf5186bafde65cbfa3db;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index 84cde74dd..e22402d9f 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -55,6 +55,7 @@ definition setoid1_of_setoid: setoid → setoid1.
 qed.
 
 coercion setoid1_of_setoid.
+prefer coercion Type_OF_setoid.
 
 definition reflexive2: ∀A:Type2.∀R:A→A→CProp2.CProp2 ≝ λA:Type2.λR:A→A→CProp2.∀x:A.R x x.
 definition symmetric2: ∀A:Type2.∀R:A→A→CProp2.CProp2 ≝ λC:Type2.λlt:C→C→CProp2. ∀x,y:C.lt x y → lt y x.
@@ -85,6 +86,10 @@ definition setoid2_of_setoid1: setoid1 → setoid2.
 qed.
 
 coercion setoid2_of_setoid1.
+prefer coercion Type_OF_setoid2. 
+prefer coercion Type_OF_setoid. 
+prefer coercion Type_OF_setoid1. 
+(* we prefer 0 < 1 < 2 *)
 
 interpretation "setoid2 eq" 'eq x y = (eq_rel2 _ (eq2 _) x y).
 interpretation "setoid1 eq" 'eq x y = (eq_rel1 _ (eq1 _) x y).