X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Fmodel.ma;h=002c1b43743e398712398f182efbd4451df1865d;hb=ce3886fa05ff0a2fbd4d7b6cf68225d90686eafe;hp=5cf20ea717b447e76df018835a546d20ebdb97d1;hpb=21f1fb39b5e1187ef87387f20522e60abe4f7c19;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/freescale/model.ma b/helm/software/matita/contribs/assembly/freescale/model.ma
index 5cf20ea71..002c1b437 100644
--- a/helm/software/matita/contribs/assembly/freescale/model.ma
+++ b/helm/software/matita/contribs/assembly/freescale/model.ma
@@ -87,10 +87,15 @@ inductive any_mcu_model : Type ≝
 | FamilyHCS08 : HCS08_mcu_model → any_mcu_model
 | FamilyRS08  : RS08_mcu_model → any_mcu_model.
 
-coercion FamilyHC05.
-coercion FamilyHC08.
-coercion FamilyHCS08.
-coercion FamilyRS08.
+definition c_FamilyHC05:= FamilyHC05.
+definition c_FamilyHC08:= FamilyHC08.
+definition c_FamilyHCS08:=FamilyHCS08.
+definition c_FamilyRS08:= FamilyRS08.
+
+coercion c_FamilyHC05.
+coercion c_FamilyHC08.
+coercion c_FamilyHCS08.
+coercion c_FamilyRS08.
 
 (* 
 condizioni errore interne alla MCU