...

[helm.git] / helm / software / matita / nlibrary / algebra / magmas.ma

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index 24203f2098422059a1fc6ec95396267cb5b0b91b..3e4cb942b4c09ba22e4188c3239748a915968fba 100644 (file)
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -24,9 +24,15 @@ nrecord magma (A: magma_type) : Type[1] ≝
    op_closed: ∀x,y. x ∈ mcarr → y ∈ mcarr → op A x y ∈ mcarr
  }.
 
+alias symbol "hint_decl" = "hint_decl_Type2".
+unification hint 0 ≔ 
+  A : ? ⊢ carr1 (qpowerclass_setoid A) ≡ qpowerclass A. 
+
+(*
 ncoercion mcarr' : ∀A. ∀M: magma A. carr1 (qpowerclass_setoid (mtcarr A))
  ≝ λA.λM: magma A.mcarr ? M
  on _M: magma ? to carr1 (qpowerclass_setoid (mtcarr ?)).
+*)
 
 nrecord magma_morphism_type (A,B: magma_type) : Type[0] ≝
  { mmcarr:> unary_morphism A B;