many changes regarding coercions:

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / categories.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index 84cde74dddc6ec669e2c8ee68232104e186c4d95..e22402d9f52542745b29e226597fe74a14920622 100644 (file)
--- 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).