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

renamed the coercion
---

diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma
index 6cb994812..884e0c582 100644
--- a/helm/software/matita/library/algebra/groups.ma
+++ b/helm/software/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.