snapshot for CSC

[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..775cbd390c4ec9287fba0148c22ebe0014d0e776 100644 (file)
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -24,9 +24,14 @@ nrecord magma (A: magma_type) : Type[1] ≝
    op_closed: ∀x,y. x ∈ mcarr → y ∈ mcarr → op A x y ∈ mcarr
  }.
 
+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;