non uniform coercions landed in hints_declaration.ma, setoids and sets library

[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 622c9401d08aec0ce1e66b3010c8c781c1b25322..4ab57d568860ad1c4b505323f909eda3cbd39573 100644 (file)
--- a/helm/software/matita/nlibrary/sets/setoids1.ma
+++ b/helm/software/matita/nlibrary/sets/setoids1.ma
@@ -21,6 +21,12 @@ nrecord setoid1: Type[2] ≝ {
   eq1: equivalence_relation1 carr1 
 }.
 
+unification hint 0 ≔ R : setoid1; 
+   MR ≟ (carr1 R), 
+   lock ≟ mk_lock2 Type[1] MR setoid1 R 
+(* ---------------------------------------- *) ⊢ 
+   setoid1 ≡ force2 ? MR lock.
+
 ndefinition setoid1_of_setoid: setoid → setoid1.
  #s; @ (carr s); @ (eq0…) (refl…) (sym…) (trans…);
 nqed.
@@ -102,10 +108,8 @@ unification hint 0 ≔ o1,o2,o3:setoid1,f:o2 ⇒_1 o3,g:o1 ⇒_1 o2;
                               fun11 ?? R ≡ (composition1 … f g).
                               
 ndefinition comp1_binary_morphisms:
- ∀o1,o2,o3.
-   (unary_morphism1_setoid1 o2 o3) ⇒_1
-     (unary_morphism1_setoid1 (unary_morphism1_setoid1 o1 o2) (unary_morphism1_setoid1 o1 o3)).
+ ∀o1,o2,o3. (o2 ⇒_1 o3) ⇒_1 ((o1 ⇒_1 o2) ⇒_1 (o1 ⇒_1 o3)).
 #o1; #o2; #o3; napply mk_binary_morphism1
- [ #f; #g; napply (comp1_unary_morphisms … f g) (*CSC: why not ∘?*)
+ [ #f; #g; napply (comp1_unary_morphisms … f g) 
  | #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ]
 nqed.