X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Fmodel.ma;h=5cf20ea717b447e76df018835a546d20ebdb97d1;hb=bf8fe5331d6e6d2dfe955efa54b1ffdafaae8429;hp=7ab85a5c7a5c8e1866b750e4303847290d4a63cf;hpb=661ffd4d7c77fce52fb2f2d96f1737be424af3f1;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/freescale/model.ma b/helm/software/matita/contribs/assembly/freescale/model.ma
index 7ab85a5c7..5cf20ea71 100644
--- a/helm/software/matita/contribs/assembly/freescale/model.ma
+++ b/helm/software/matita/contribs/assembly/freescale/model.ma
@@ -87,10 +87,10 @@ inductive any_mcu_model : Type ≝
 | FamilyHCS08 : HCS08_mcu_model → any_mcu_model
 | FamilyRS08  : RS08_mcu_model → any_mcu_model.
 
-coercion cic:/matita/freescale/model/any_mcu_model.ind#xpointer(1/1/1).
-coercion cic:/matita/freescale/model/any_mcu_model.ind#xpointer(1/1/2).
-coercion cic:/matita/freescale/model/any_mcu_model.ind#xpointer(1/1/3).
-coercion cic:/matita/freescale/model/any_mcu_model.ind#xpointer(1/1/4).
+coercion FamilyHC05.
+coercion FamilyHC08.
+coercion FamilyHCS08.
+coercion FamilyRS08.
 
 (* 
 condizioni errore interne alla MCU