a) update with upstream version

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

diff --git a/helm/software/matita/contribs/assembly/freescale/opcode.ma b/helm/software/matita/contribs/assembly/freescale/opcode.ma
index 47312085f146a5c58f104da6e63ddc4a27b17897..fc30ddeb414e309efc92d2a6bd2c39b1b26c6873 100644 (file)
--- a/helm/software/matita/contribs/assembly/freescale/opcode.ma
+++ b/helm/software/matita/contribs/assembly/freescale/opcode.ma
@@ -216,15 +216,15 @@ inductive opcode: Type ≝
 inductive any_opcode (m:mcu_type) : Type ≝
  anyOP : opcode → any_opcode m.
 
-coercion cic:/matita/freescale/opcode/any_opcode.ind#xpointer(1/1/1).
+coercion anyOP.
 
 (* raggruppamento di byte e word in un tipo unico *)
 inductive byte8_or_word16 : Type ≝
   Byte: byte8  → byte8_or_word16
 | Word: word16 → byte8_or_word16.
 
-coercion cic:/matita/freescale/opcode/byte8_or_word16.ind#xpointer(1/1/1).
-coercion cic:/matita/freescale/opcode/byte8_or_word16.ind#xpointer(1/1/2).
+coercion Byte.
+coercion Word.
 
 (* opcode → naturali, per usare eqb *)
 definition magic_of_opcode ≝