nasty change in the lexer/parser:

[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 fc30ddeb414e309efc92d2a6bd2c39b1b26c6873..7b891bc8814122a41470b5e5e76002733893ac21 100644 (file)
--- a/helm/software/matita/contribs/assembly/freescale/opcode.ma
+++ b/helm/software/matita/contribs/assembly/freescale/opcode.ma
@@ -216,15 +216,20 @@ inductive opcode: Type ≝
 inductive any_opcode (m:mcu_type) : Type ≝
  anyOP : opcode → any_opcode m.
 
-coercion anyOP.
+definition c_anyOP ≝ anyOP.
+
+coercion c_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 Byte.
-coercion Word.
+definition c_Byte ≝ Byte.
+definition c_Word ≝ Word.
+
+coercion c_Byte.
+coercion c_Word.
 
 (* opcode → naturali, per usare eqb *)
 definition magic_of_opcode ≝