many changes regarding coercions:

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / o-algebra.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
index 8ff55d0d6d60dee44c18e529cdd67245517c57d9..ca3d0379b2dcb0fe6bd99ce24656b146e0ce86c1 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -137,6 +137,8 @@ qed.
 interpretation "o-algebra binary meet" 'and a b = 
   (fun21 ___ (binary_meet _) a b).
 
+prefer coercion Type1_OF_OAlgebra.
+
 definition binary_join : ∀O:OAlgebra. binary_morphism1 O O O.
 intros; split;
 [ intros (p q); 
@@ -151,8 +153,6 @@ qed.
 interpretation "o-algebra binary join" 'or a b = 
   (fun21 ___ (binary_join _) a b).
 
-coercion Type1_OF_OAlgebra nocomposites.
-
 lemma oa_overlap_preservers_meet: ∀O:OAlgebra.∀p,q:O.p >< q → p >< (p ∧ q).
 (* next change to avoid universe inconsistency *)
 change in ⊢ (?→%→%→?) with (Type1_OF_OAlgebra O);
@@ -260,15 +260,17 @@ qed.
 coercion umorphism_setoid_OF_ORelation_setoid.
 
 lemma uncurry_arrows : ∀B,C. ORelation_setoid B C → B → C. 
-intros; apply ((fun11 ?? t) t1);
+intros; apply (t t1);
 qed.
 
 coercion uncurry_arrows 1.
 
+(*
 lemma hint6: ∀P,Q. Type_OF_setoid2 (hint5 P ⇒ hint5 Q) → unary_morphism1 P Q.
  intros; apply t;
 qed.
 coercion hint6.
+*)
 
 notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}.
 notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}.