X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Fword16.ma;h=d5bdd68bf06aed722d91093953f1a36ce053468b;hb=842e243be954d67360788d08701289f3237c2699;hp=98d7703b636db370c1b85225f423986b4c3379d2;hpb=661ffd4d7c77fce52fb2f2d96f1737be424af3f1;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/freescale/word16.ma b/helm/software/matita/contribs/assembly/freescale/word16.ma
index 98d7703b6..d5bdd68bf 100644
--- a/helm/software/matita/contribs/assembly/freescale/word16.ma
+++ b/helm/software/matita/contribs/assembly/freescale/word16.ma
@@ -39,8 +39,7 @@ record word16 : Type ≝
 (* \langle \rangle *)
 notation "〈x:y〉" non associative with precedence 80
  for @{ 'mk_word16 $x $y }.
-interpretation "mk_word16" 'mk_word16 x y = 
- (cic:/matita/freescale/word16/word16.ind#xpointer(1/1/1) x y).
+interpretation "mk_word16" 'mk_word16 x y = (mk_word16 x y).
 
 (* operatore = *)
 definition eq_w16 ≝ λw1,w2.(eq_b8 (w16h w1) (w16h w2)) ⊗ (eq_b8 (w16l w1) (w16l w2)).
@@ -151,7 +150,7 @@ definition MSB_w16 ≝ λw:word16.eq_ex x8 (and_ex x8 (b8h (w16h w))).
 (* word → naturali *)
 definition nat_of_word16 ≝ λw:word16. 256 * (w16h w) + (nat_of_byte8 (w16l w)).
 
-coercion cic:/matita/freescale/word16/nat_of_word16.con.
+coercion nat_of_word16.
 
 (* naturali → word *)
 definition word16_of_nat ≝