From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 10 Jul 2006 17:07:49 +0000 (+0000)
Subject: renamed the coercion
X-Git-Tag: 0.4.95@7852~1235
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=92315dd030151c0eb8afda77bc83076d043bd8ce;p=helm.git

renamed the coercion
---

diff --git a/matita/library/algebra/groups.ma b/matita/library/algebra/groups.ma
index 6cb994812..884e0c582 100644
--- a/matita/library/algebra/groups.ma
+++ b/matita/library/algebra/groups.ma
@@ -190,7 +190,7 @@ for @{ 'subgroupimage $H $x }.
 
 interpretation "Subgroup image" 'subgroupimage H x =
  (cic:/matita/algebra/groups/image.con _ _
-   (cic:/matita/algebra/groups/morphism_of_subgroup.con _ H) x).
+   (cic:/matita/algebra/groups/morphism_OF_subgroup.con _ H) x).
 
 definition member_of_subgroup ≝
  λG.λH:subgroup G.λx:G.∃y.x=y \sub H.