Procedural: higher-order unification needs a lot of hints !!

[helm.git] / helm / software / matita / contribs / assembly / freescale / model.ma

diff --git a/helm/software/matita/contribs/assembly/freescale/model.ma b/helm/software/matita/contribs/assembly/freescale/model.ma
index 7ab85a5c7a5c8e1866b750e4303847290d4a63cf..002c1b43743e398712398f182efbd4451df1865d 100644 (file)
--- 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 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).
+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