maction support added to notation, adopted for = AKA = \sub t

[helm.git] / helm / software / matita / library / algebra / groups.ma

diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma
index f257951bc4a031abb0a1640ac0c673da3e6b340c..d6e77ae8d0fa6a36404b7d084911e12602c234de 100644 (file)
--- a/helm/software/matita/library/algebra/groups.ma
+++ b/helm/software/matita/library/algebra/groups.ma
@@ -218,8 +218,8 @@ definition left_coset_eq ≝
  λG.λC,C':left_coset G.
   ∀x.((element ? C)·x \sub (subgrp ? C)) ∈ C'.
   
-interpretation "Left cosets equality" 'eq C C' =
- (cic:/matita/algebra/groups/left_coset_eq.con _ C C').
+interpretation "Left cosets equality" 'eq t C C' =
+ (cic:/matita/algebra/groups/left_coset_eq.con t C C').
 
 definition left_coset_disjoint ≝
  λG.λC,C':left_coset G.